iff_ortho_complete — Mathlib

English

For commutative semirings, CompleteOrthogonalIdempotents ![x, y] holds iff 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

/-- If a family is complete orthogonal, it consists of idempotents. -/
theorem iff_ortho_complete : CompleteOrthogonalIdempotents e ↔ Pairwise (e · * e · = 0) ∧ ∑ i, e i = 1 :=
  by
  rw [completeOrthogonalIdempotents_iff, orthogonalIdempotents_iff, and_assoc, and_iff_right_of_imp]
  intro ⟨ortho, complete⟩ i
  apply_fun (e i * ·) at complete
  rwa [Finset.mul_sum, Finset.sum_eq_single i (fun _ _ ne ↦ ortho ne.symm) (by simp at ·), mul_one] at complete

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