English
For any square matrices A, B, adj(A B) = adj(B) adj(A).
Русский
Для любых квадратных матриц A, B: adj(A B) = adj(B) adj(A).
LaTeX
$$$\operatorname{adj}(A B) = \operatorname{adj}(B) \operatorname{adj}(A)$$$
Lean4
/-- Proof follows from "The trace Cayley-Hamilton theorem" by Darij Grinberg, Section 5.3
-/
theorem adjugate_mul_distrib (A B : Matrix n n α) : adjugate (A * B) = adjugate B * adjugate A :=
by
let g : Matrix n n α → Matrix n n α[X] := fun M => M.map Polynomial.C + (Polynomial.X : α[X]) • (1 : Matrix n n α[X])
let f' : Matrix n n α[X] →+* Matrix n n α := (Polynomial.evalRingHom 0).mapMatrix
have f'_inv : ∀ M, f' (g M) = M := by
intro
ext
simp [f', g]
have f'_adj : ∀ M : Matrix n n α, f' (adjugate (g M)) = adjugate M :=
by
intro
rw [RingHom.map_adjugate, f'_inv]
have f'_g_mul : ∀ M N : Matrix n n α, f' (g M * g N) = M * N :=
by
intro M N
rw [RingHom.map_mul, f'_inv, f'_inv]
have hu : ∀ M : Matrix n n α, IsRegular (g M).det := by
intro M
refine Polynomial.Monic.isRegular ?_
simp only [g, Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]
rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ← adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left,
RingHom.map_adjugate, RingHom.map_adjugate, f'_inv, f'_g_mul]
