English
In an integrally closed domain, for nonzero n, Associated(a^n, b^n) is equivalent to Associated(a,b).
Русский
В интегрально замкнутом домене при ненулевом n соотношение Associated(a^n, b^n) эквивалентно Associated(a,b).
LaTeX
$$$Associated(a^n, b^n) \iff Associated(a, b) \quad (n\neq 0)$$$
Lean4
@[simp]
theorem pow_dvd_pow_iff [IsDomain R] [IsIntegrallyClosed R] {n : ℕ} (hn : n ≠ 0) {a b : R} : a ^ n ∣ b ^ n ↔ a ∣ b :=
by
refine ⟨fun ⟨x, hx⟩ ↦ ?_, fun h ↦ pow_dvd_pow_of_dvd h n⟩
by_cases ha : a = 0
· simpa [ha, hn] using hx
let K := FractionRing R
replace ha : algebraMap R K a ≠ 0 := fun h ↦ ha <| (injective_iff_map_eq_zero _).1 (IsFractionRing.injective R K) _ h
let y := (algebraMap R K b) / (algebraMap R K a)
have hy : IsIntegral R y := by
refine ⟨X ^ n - C x, monic_X_pow_sub_C _ hn, ?_⟩
simp only [y, eval₂_sub, eval₂_X_pow, div_pow, eval₂_C]
replace hx := congr_arg (algebraMap R K) hx
rw [map_pow] at hx
simp [hx, ha]
obtain ⟨k, hk⟩ := algebraMap_eq_of_integral hy
refine ⟨k, IsFractionRing.injective R K ?_⟩
rw [map_mul, hk, mul_div_cancel₀ _ ha]
