adjugate_fin_one

Mathlib.LinearAlgebra.Matrix.Adjugate

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

English

For size Fin 1, adjugate is identity: adjugate(1) = 1.

Русский

Для размера Fin 1 adjugate(1) = 1.

LaTeX

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

Lean4

@[simp]
theorem adjugate_fin_one (A : Matrix (Fin 1) (Fin 1) α) : adjugate A = 1 :=
  adjugate_subsingleton A

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

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

Разделы

Аффилиация

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