pair_iff'ₛ — Mathlib

English

In a commutative semiring, CompleteOrthogonalIdempotents ![x, y] is equivalent to x y = 0 and x + y = 1.

Русский

В коммутативном полукольце, CompleteOrthogonalIdempotents ![x, y] эквивалентно x y = 0 и x + y = 1.

LaTeX

$$CompleteOrthogonalIdempotents ![x, y] ↔ x y = 0 ∧ x + y = 1$$

Lean4

theorem pair_iff'ₛ {x y : R} : CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ y * x = 0 ∧ x + y = 1 := by
  simp [iff_ortho_complete, Pairwise, Fin.forall_fin_two, and_assoc]

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