pair_iff — Mathlib

English

Two elements x,y in a ring form a complete pair of orthogonal idempotents iff x is idempotent and y = 1 − x.

Русский

Два элемента x, y кольца образуют полную пару ортогональных идемпотентов тогда и только тогда, когда x идемпотент и y = 1 − x.

LaTeX

$$$CompleteOrthogonalIdempotents([x, y]) \\iff (IsIdempotentElem(x) \\wedge y = 1 - x)$$$

Lean4

theorem pair_iff {x y : R} : CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x :=
  by
  rw [pair_iff'ₛ, ← eq_sub_iff_add_eq', ← and_assoc, and_congr_left_iff]
  rintro rfl
  simp [mul_sub, sub_mul, IsIdempotentElem, sub_eq_zero, eq_comm]

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