adjugate_def

Mathlib.LinearAlgebra.Matrix.Adjugate

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

English

The adjugate of A equals the matrix whose i-th row is cramer Aᵀ (Pi.single i 1).

Русский

Adjugate A равно матрице, где i-я строка задаётся как cramer Aᵀ (e_i).

LaTeX

$$$$\\operatorname{adjugate}(A) = \\operatorname{of} \\; i \\mapsto \\mathrm{cramer}(A^{\\top}, \\mathbf{e}_i).$$$$

Lean4

theorem adjugate_def (A : Matrix n n α) : adjugate A = of fun i => cramer Aᵀ (Pi.single i 1) :=
  rfl

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

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

Разделы

Аффилиация

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