English
Let S be a Dedekind domain and P a prime ideal with P ≠ ⊥. For a,d,d',e,e' ∈ S, if a ∉ P^{i+1}, e,e' ∈ P^{i+1}, and a d + e − (a d' + e') ∈ P^{i+1}, then d − d' ∈ P.
Русский
Пусть S — область Дедекнда, P — простой идеал, не равный нулю. Для a,d,d',e,e' ∈ S, если a ∉ P^{i+1}, e,e' ∈ P^{i+1}, и a d + e − (a d' + e') ∈ P^{i+1}, то d − d' ∈ P.
LaTeX
$$$[\\text{IsDedekindDomain } S]\\; (hP : P \\neq \\bottom) \\rightarrow \\forall i\\in\\mathbb{N}, a,d,d',e,e' \\in S:\\; a \\notin P^{i+1} \\land e,e' \\in P^{i+1} \\land (a d + e - (a d' + e')) \\in P^{i+1} \\Rightarrow d - d' \\in P$$$
Lean4
/-- The choice of `d` in `Ideal.exists_mul_add_mem_pow_succ` is unique, up to `P`.
Inspired by [Neukirch], proposition 6.1 -/
theorem mul_add_mem_pow_succ_unique [IsDedekindDomain S] (hP : P ≠ ⊥) {i : ℕ} (a d d' e e' : S)
(a_notMem : a ∉ P ^ (i + 1)) (e_mem : e ∈ P ^ (i + 1)) (e'_mem : e' ∈ P ^ (i + 1))
(h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)) : d - d' ∈ P :=
by
have h' : a * (d - d') ∈ P ^ (i + 1) :=
by
convert Ideal.add_mem _ h (Ideal.sub_mem _ e'_mem e_mem) using 1
ring
exact Ideal.mem_prime_of_mul_mem_pow hP a_notMem h'
