one_apply_eq

Mathlib.Data.Matrix.Diagonal

URI: https://scilib.ai/kg/mathlib#Matrix.one_apply_eq

English

For AddMonoidWithOne α, the entry (i,j) of (d : Matrix n n α) is d if i=j and 0 otherwise.

Русский

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

LaTeX

$$$(d : Matrix n n α)_{ij} = \begin{cases} d, & i=j \\ 0, & i\neq j \end{cases}$$$

Lean4

@[simp]
theorem one_apply_eq (i) : (1 : Matrix n n α) i i = 1 :=
  diagonal_apply_eq _ i

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru