diag — Mathlib

English

diag i j is the identity map if i=j and the zero map otherwise.

Русский

diag i j равен тождественному отображению, если i=j, иначе нулевому отображению.

LaTeX

$$$\\mathrm{diag}(i,j) : \\phi_i \\to \\phi_j := \\text{identity if } i=j, \\text{ else } 0.$$$

Lean4

/-- `diag i j` is the identity map if `i = j`. Otherwise it is the constant 0 map. -/
def diag (i j : ι) : φ i →ₗ[R] φ j :=
  @Function.update ι (fun j => φ i →ₗ[R] φ j) _ 0 i id j

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