compl_apply_diag

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

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

English

The diagonal entries of A.compl are zero.

Русский

Диагональные элементы A.compl равны нулю.

LaTeX

$$$(A.compl)_{ii} = 0$$$

Lean4

@[simp]
theorem compl_apply_diag [Zero α] [One α] (i : V) : A.compl i i = 0 := by simp [compl]

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

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

Разделы

Аффилиация

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