English
If A is an n×n matrix with n ≥ 2 (i.e., not 1×1), then adj(adj(A)) = det(A)^(n−2) · A.
Русский
Если A — матрица размерности n×n с n ≥ 2, то adj(adj(A)) = det(A)^(n−2) · A.
LaTeX
$$$\\operatorname{adj}(\\operatorname{adj}(A)) = \\det(A)^{(n-2)} \\cdot A$$$
Lean4
/-- Note that this is not true for `Fintype.card n = 1` since `1 - 2 = 0` and not `-1`. -/
theorem adjugate_adjugate (A : Matrix n n α) (h : Fintype.card n ≠ 1) :
adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A := by
-- get rid of the `- 2`
rcases h_card : Fintype.card n with _ | n'
· subsingleton [Fintype.card_eq_zero_iff.mp h_card]
cases n'
· exact (h h_card).elim
rw [← h_card]
-- express `A` as an evaluation of a polynomial in n^2 variables, and solve in the polynomial ring
-- where `A'.det` is non-zero.
let A' := mvPolynomialX n n ℤ
suffices adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A' by
rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this, ← AlgHom.map_det, ←
map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2), AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply,
Matrix.map_smul' _ _ _ (map_mul _)]
have h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1 := by simp [h_card]
have is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A') := fun x y =>
mul_left_cancel₀ (det_mvPolynomialX_ne_zero n ℤ)
apply is_reg.matrix
simp only
rw [smul_smul, ← pow_succ', h_card', det_smul_adjugate_adjugate]
