iff_eq_zero_or_one — Mathlib

English

In a CancelMonoidWithZero, any element p with p^2 = p must be either 0 or 1. Equivalently, IsIdempotentElem p holds iff p = 0 or p = 1.

Русский

В CancelMonoidWithZero любое идемпотентное p должно быть либо 0, либо 1. Иначе IsIdempotentElem p эквивалентно p = 0 или p = 1.

LaTeX

$$$ IsIdempotentElem(p) \iff p = 0 \lor p = 1. $$$

Lean4

@[simp]
theorem iff_eq_zero_or_one {p : G₀} : IsIdempotentElem p ↔ p = 0 ∨ p = 1
    where
  mp h := or_iff_not_imp_left.mpr fun hp ↦ mul_left_cancel₀ hp (h.trans (mul_one p).symm)
  mpr h := h.elim (fun hp => hp.symm ▸ zero) fun hp => hp.symm ▸ one

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