iff_eq_one_of_isUnit — Mathlib

English

If a is a unit, then a is idempotent iff a = 1.

Русский

Если a является единицей, то a идемпотентен тогда и только тогда, когда a = 1.

LaTeX

$$$\\text{IsUnit}(a) \\; \\Rightarrow \\; \\text{IsIdempotentElem}(a) \\iff a = 1.$$$

Lean4

theorem iff_eq_one_of_isUnit (h : IsUnit a) : IsIdempotentElem a ↔ a = 1
    where
  mp
    idem := by
    have ⟨q, eq⟩ := h.exists_left_inv
    rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]
  mpr := by rintro rfl; exact .one

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