iff_mul_eq — Mathlib

English

An indexed family e: I → R is an orthogonal idempotent family if and only if for all i,j we have e_i e_j = δ_{ij} e_i.

Русский

Семейство e: I → R является ортогональными идемпотентами тогда и только тогда, когда для всех i,j выполняется e_i e_j = δ_{ij} e_i.

LaTeX

$$OrthogonalIdempotents(e) iff ∀ i j, e_i e_j = δ_{ij} e_i$$

Lean4

theorem iff_mul_eq [DecidableEq I] : OrthogonalIdempotents e ↔ ∀ i j, e i * e j = if i = j then e i else 0 :=
  ⟨mul_eq, fun H ↦ ⟨fun i ↦ by simpa using H i i, fun i j e ↦ by simpa [e] using H i j⟩⟩

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