id_def

Mathlib.CategoryTheory.Preadditive.Mat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Mat.id_def

English

The (i,i)-entry of the identity matrix is 1 for every i.

Русский

Для каждого индекса i диагональный элемент единичной матрицы равен 1.

LaTeX

$$$\big( \mathsf{Id}_M \big)_{ii} = 1$$$

Lean4

theorem id_def (M : Mat R) : 𝟙 M = fun i j => if i = j then 1 else 0 :=
  rfl

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

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

Разделы

Аффилиация

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