toMatrix_transpose_apply

Mathlib.LinearAlgebra.Matrix.Basis

URI: https://scilib.ai/kg/mathlib#Module.Basis.toMatrix_transpose_apply

English

Same weak adjugate-adjugate identity as in 129981, interpreted under the same nontriviality assumption.

Русский

Та же слабая формула adj(adj(A)) = det(A)^(n−2) A под тем же условием ненулевого размера.

LaTeX

$$$\\operatorname{adj}(\\operatorname{adj}(A)) = \\det(A)^{(n-2)} \\cdot A$$$

Lean4

theorem toMatrix_transpose_apply : (e.toMatrix v)ᵀ j = e.repr (v j) :=
  funext fun _ => rfl

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

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

Разделы

Аффилиация

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