adjugate_eq_one_of_card_eq_one

Mathlib.LinearAlgebra.Matrix.Adjugate

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

← MathLib Explorer

English

For A in matrices of size Fin 0, adjugate A = 0.

Русский

Для матрицы A размера Fin 0 адъюгат равен нулю.

LaTeX

$$$\operatorname{adj}(A) = 0 \quad \text{when } n = 0$$$

Lean4

theorem adjugate_eq_one_of_card_eq_one {A : Matrix n n α} (h : Fintype.card n = 1) : adjugate A = 1 :=
  haveI : Subsingleton n := Fintype.card_le_one_iff_subsingleton.mp h.le
  adjugate_subsingleton _

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

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

Разделы

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

Аффилиация

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