English
Let P be an ideal in a commutative ring S, and let i be a natural number. If a ∈ P^i, e ∈ P^{i+1}, e' ∈ P^{i+1}, and d − d' ∈ P, then a d + e − (a d' + e') ∈ P^{i+1}.
Русский
Пусть P — идеал в коммутативном кольце S, пусть i ∈ ℕ. Если a ∈ P^i, e ∈ P^{i+1}, e' ∈ P^{i+1}, и d − d' ∈ P, то a d + e − (a d' + e') ∈ P^{i+1}.
LaTeX
$$$\\forall S [\\text{CommRing } S], \\forall P\\,\\text{Ideal } S, i \\in \\mathbb{N},\\; a,d,d',e,e' \\in S:\\; a \\in P^i \\land e \\in P^{i+1} \\land e' \\in P^{i+1} \\land (d - d') \\in P \\Rightarrow a \\cdot d + e - (a \\cdot d' + e') \\in P^{i+1}$$$
Lean4
/-- If the `d` from `Ideal.exists_mul_add_mem_pow_succ` is unique, up to `P`,
then so are the `c`s, up to `P ^ (i + 1)`.
Inspired by [Neukirch], proposition 6.1 -/
theorem mul_add_mem_pow_succ_inj (P : Ideal S) {i : ℕ} (a d d' e e' : S) (a_mem : a ∈ P ^ i) (e_mem : e ∈ P ^ (i + 1))
(e'_mem : e' ∈ P ^ (i + 1)) (h : d - d' ∈ P) : a * d + e - (a * d' + e') ∈ P ^ (i + 1) :=
by
have : a * d - a * d' ∈ P ^ (i + 1) := by
simp only [← mul_sub]
exact Ideal.mul_mem_mul a_mem h
convert Ideal.add_mem _ this (Ideal.sub_mem _ e_mem e'_mem) using 1
ring
