English
A technical auxiliary result: adjugate of a product can be expressed via an auxiliary polynomial map; used to derive a general distributive property.
Русский
Технический вспомогательный результат: adjugate произведения может быть выражена через дополнительное отображение, используемое для вывода общих свойств.
LaTeX
$$$\text{auxiliary: } \operatorname{adj}(A B) = \operatorname{adj}(B) \operatorname{adj}(A) \; \text{under suitable hypotheses}$$$
Lean4
theorem adjugate_mul_distrib_aux (A B : Matrix n n α) (hA : IsLeftRegular A.det) (hB : IsLeftRegular B.det) :
adjugate (A * B) = adjugate B * adjugate A :=
by
have hAB : IsLeftRegular (A * B).det := by
rw [det_mul]
exact hA.mul hB
refine (isRegular_of_isLeftRegular_det hAB).left ?_
simp only
rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate, smul_mul, Matrix.one_mul, mul_smul,
mul_adjugate, smul_smul, mul_comm, ← det_mul]
