cotangent_subsingleton_iff — Mathlib

English

Subsingleton I.Cotangent is equivalent to I being idempotent (I^2 = I).

Русский

Подмодуль I.Cotangent является одиничным тогда и только тогда, когда I идемпотентен (I^2 = I).

LaTeX

$$$\\text{Subsingleton } I.Cotangent \\iff \\text{IsIdempotentElem } I$$$

Lean4

theorem cotangent_subsingleton_iff : Subsingleton I.Cotangent ↔ IsIdempotentElem I :=
  by
  constructor
  · intro H
    refine (pow_two I).symm.trans (le_antisymm (Ideal.pow_le_self two_ne_zero) ?_)
    exact fun x hx => (I.toCotangent_eq_zero ⟨x, hx⟩).mp (Subsingleton.elim _ _)
  ·
    exact fun e =>
      ⟨fun x y =>
        Quotient.inductionOn₂' x y fun x y =>
          I.toCotangent_eq.mpr <| ((pow_two I).trans e).symm ▸ I.sub_mem x.prop y.prop⟩

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