English
Let S be a Dedekind domain and P a prime ideal. If a ∉ P^{i+1} and a b ∈ P^{i+1}, then b ∈ P.
Русский
Пусть S — область Дедекнда, P — простой идеал. Если a ∉ P^{i+1} и a b ∈ P^{i+1}, то b ∈ P.
LaTeX
$$$[\\text{IsDedekindDomain } S]\\; {P : \\text{Ideal } S}\\; (hP : P \\neq \\bottom) \\;\\rightarrow\\; \\forall i\\in\\mathbb{N}, a,b\\in S:\\; a \\notin P^{i+1} \\land a b \\in P^{i+1} \\Rightarrow b \\in P$$$
Lean4
theorem mem_prime_of_mul_mem_pow [IsDedekindDomain S] {P : Ideal S} [P_prime : P.IsPrime] (hP : P ≠ ⊥) {i : ℕ} {a b : S}
(a_notMem : a ∉ P ^ (i + 1)) (ab_mem : a * b ∈ P ^ (i + 1)) : b ∈ P :=
by
simp only [← Ideal.span_singleton_le_iff_mem, ← Ideal.dvd_iff_le, pow_succ,
← Ideal.span_singleton_mul_span_singleton] at a_notMem ab_mem ⊢
exact (prime_pow_succ_dvd_mul (Ideal.prime_of_isPrime hP P_prime) ab_mem).resolve_left a_notMem
