instOne — Mathlib

English

The unit of the incidence algebra is the delta function, with entries 1 on the diagonal and 0 off-diagonal.

Русский

Единичный элемент инцидентной алгебры — дельта-функция: на диагонали — 1, вне диагонали — 0.

LaTeX

$$$ (1 : IncidenceAlgebra 𝕜 α) a b = \begin{cases} 1 & a = b \\ 0 & a \neq b \end{cases} $$$

Lean4

/-- The unit incidence algebra is the delta function, whose entries are `0` except on the diagonal
where they are `1`. -/
instance instOne : One (IncidenceAlgebra 𝕜 α) :=
  ⟨⟨fun a b ↦ if a = b then 1 else 0, fun _a _b h ↦ ite_eq_right_iff.2 fun H ↦ (h H.le).elim⟩⟩

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