mul_eq — Mathlib

English

If (e_i)_{i ∈ I} is a family of orthogonal idempotents in a semiring R, then for all i,j in I, e_i e_j equals e_i when i = j and equals 0 otherwise.

Русский

Если семейство идемпотентов {e_i} индексировано I состоит из ортогональных идемпотентов в полукольце R, то произведение e_i e_j равно e_i при i = j и равно нулю при i ≠ j.

LaTeX

$$$e_i e_j = \begin{cases} e_i, & i=j \\ 0, & i\neq j \end{cases}$$$

Lean4

theorem mul_eq [DecidableEq I] (he : OrthogonalIdempotents e) (i j) : e i * e j = if i = j then e i else 0 :=
  by
  split
  · simp [*, (he.idem j).eq]
  · exact he.ortho ‹_›

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