natCast_apply — Mathlib

English

For AddMonoidWithOne α, the entry (i,j) of d cast equals d if i=j and 0 otherwise.

Русский

Для AddMonoidWithOne α элемент матрицы (i,j) равен d, если i=j, и 0, если i≠j.

LaTeX

$$$(d : Matrix n n α)_{ij} = \begin{cases} d, & \text{если } i=j, \\ 0, & \text{иначе} \end{cases}$$$

Lean4

theorem natCast_apply [AddMonoidWithOne α] {i j} {d : ℕ} : (d : Matrix n n α) i j = if i = j then d else 0 := by
  rw [Nat.cast_ite, Nat.cast_zero, ← diagonal_natCast, diagonal_apply]

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