eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute

English

If e1,e2 are idempotent in a ring, e1−e2 is nilpotent, and e1,e2 commute, then e1 = e2.

Русский

Если e1,e2 — идемпотенты, разность e1−e2 нильпотентна и они commute, то e1 = e2.

LaTeX

$$$IsNilpotent(e1 - e2) \\wedge Commute(e1,e2) \\Rightarrow e1 = e2$$$

Lean4

theorem eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute {e₁ e₂ : R} (he₁ : IsIdempotentElem e₁)
    (he₂ : IsIdempotentElem e₂) (H : IsNilpotent (e₁ - e₂)) (H' : Commute e₁ e₂) : e₁ = e₂ :=
  by
  have : (e₁ - e₂) ^ 3 = (e₁ - e₂) :=
    by
    simp only [pow_succ, pow_zero, mul_sub, one_mul, sub_mul, he₁.eq, he₂.eq, H'.eq, mul_assoc]
    simp only [← mul_assoc, he₂.eq]
    abel
  obtain ⟨n, hn⟩ := H
  have : (e₁ - e₂) ^ (2 * n + 1) = (e₁ - e₂) := by clear hn;
    induction n <;> simp [mul_add, add_assoc, pow_add _ (2 * _) 3, ← pow_succ, *]
  rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this

Похожие утверждения