isDiag_one

Mathlib.LinearAlgebra.Matrix.IsDiag

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

← MathLib Explorer

English

The identity matrix is diagonal.

Русский

Единичная матрица диагональная.

LaTeX

$$$ (I_n) \ text{ IsDiag}.$$$

Lean4

/-- Every identity matrix is diagonal. -/
@[simp]
theorem isDiag_one [DecidableEq n] [Zero α] [One α] : (1 : Matrix n n α).IsDiag := fun _ _ => one_apply_ne

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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