one_eq_pi_single — Mathlib

English

For the n×n identity matrix I_n with entries in α, the (i,j) entry equals 1 if i = j and 0 otherwise; equivalently, (I_n)_{i j} = δ_{i j}.

Русский

Для единичной матрицы I_n над α элемент на позиции (i,j) равен 1 при i = j и 0 при i ≠ j; то есть (I_n)_{i j} = δ_{i j}.

LaTeX

$$$(1 : \mathrm{Matrix}\ n\ n\ α)_{ij} = \delta_{ij}$$$

Lean4

theorem one_eq_pi_single {i j} : (1 : Matrix n n α) i j = Pi.single (M := fun _ => α) i 1 j := by
  simp only [one_apply, Pi.single_apply, eq_comm]

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