English
Let P be a nonzero prime ideal in a Dedekind domain A. For any natural number i, if P^(i+1) is strictly contained in I and I is contained in P^i, then I = P^i.
Русский
Пусть P — непустой простая идеал в области Дедекында A. Для любого натурального i, если P^(i+1) строго содержится в I и I ⊆ P^i, то I = P^i.
LaTeX
$$$P^{i+1} < I \\quad\\text{and}\\quad I \\le P^i \\quad\\Longrightarrow\\quad I = P^i.$$$
Lean4
theorem eq_prime_pow_of_succ_lt_of_le {P I : Ideal A} [P_prime : P.IsPrime] (hP : P ≠ ⊥) {i : ℕ} (hlt : P ^ (i + 1) < I)
(hle : I ≤ P ^ i) : I = P ^ i := by
refine le_antisymm hle ?_
have P_prime' := Ideal.prime_of_isPrime hP P_prime
have h1 : I ≠ ⊥ := (lt_of_le_of_lt bot_le hlt).ne'
have := pow_ne_zero i hP
have h3 := pow_ne_zero (i + 1) hP
rw [← Ideal.dvdNotUnit_iff_lt, dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors h1 h3, normalizedFactors_pow,
normalizedFactors_irreducible P_prime'.irreducible, Multiset.nsmul_singleton, Multiset.lt_replicate_succ] at hlt
rw [← Ideal.dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors, normalizedFactors_pow,
normalizedFactors_irreducible P_prime'.irreducible, Multiset.nsmul_singleton]
all_goals assumption
