adjugate_zero

Mathlib.LinearAlgebra.Matrix.Adjugate

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

← MathLib Explorer

English

The adjugate of the identity matrix is the identity: adj(I) = I.

Русский

Адъюгат единичной матрицы равен единичной матрице: adj(I) = I.

LaTeX

$$$\operatorname{adj}(I_n) = I_n$$$

Lean4

@[simp]
theorem adjugate_zero [Nontrivial n] : adjugate (0 : Matrix n n α) = 0 :=
  by
  ext i j
  obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j
  apply det_eq_zero_of_column_eq_zero j'
  intro j''
  simp [updateCol_ne hj']

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

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

Разделы

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

Аффилиация

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