det_smul_adjugate_adjugate — Mathlib

English

Let A be an n×n matrix over a commutative ring. Then det(A) · adj(adj(A)) = det(A)^(n−1) · A.

Русский

Пусть A — квадратная матрица размерности n над коммутативным кольцом. Тогда det(A) · adj(adj(A)) = det(A)^(n−1) · A.

LaTeX

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

Lean4

theorem det_smul_adjugate_adjugate (A : Matrix n n α) :
    det A • adjugate (adjugate A) = det A ^ (Fintype.card n - 1) • A :=
  by
  have : A * (A.adjugate * A.adjugate.adjugate) = A * (A.det ^ (Fintype.card n - 1) • (1 : Matrix n n α)) := by
    rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
  rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul, Matrix.one_mul] at this

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