Rescaling an integral ideal by an element of its inverse ideal preserves its class and carries the chosen generator of its square to the exact generator alpha*kappa^2. This retains the generator needed for subsequent archimedean estimates, rather than replacing it by an unspecified associate.

theorem CCDN.rescale_integral_ideal_square {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (I : ↥(nonZeroDivisors (Ideal R))) {α : R} (hα : α ≠ 0) (hIα : ↑I ^ 2 = Ideal.span {α}) {κ : K} (hκ : κ ≠ 0) (hκI : κ ∈ (↑↑I)⁻¹) : ∃ (J : ↥(nonZeroDivisors (Ideal R))) (β : R), ClassGroup.mk0 J = ClassGroup.mk0 I ∧ β ≠ 0 ∧ (algebraMap R K) β = (algebraMap R K) α * κ ^ 2 ∧ ↑J ^ 2 = Ideal.span {β} ∧ ↑↑J = (FractionalIdeal.spanSingleton (nonZeroDivisors R)) κ * ↑↑I

Rescaling an integral ideal I with I ^ 2 = (α) by a nonzero κ ∈ I⁻¹ gives an integral ideal J = κ I in the same class with J ^ 2 = (β) for the exact generator β = α * κ ^ 2.