English
The coefficient of X^{card n} in det((X)·A.map C + B.map C) equals det A.
Русский
Коэффициент при степени \(X^{|n|}\) в детерминанте det((X)·A.map C + B.map C) равен det A.
LaTeX
$$$\\coeff_{\\,|n|}\\big(\\det\\big((X : \\alpha[X]) \\cdot A.map C + B.map C\\big)\\big) = \\det A$$$
Lean4
theorem coeff_det_X_add_C_card (A B : Matrix n n α) :
coeff (det ((X : α[X]) • A.map C + B.map C)) (Fintype.card n) = det A :=
by
rw [det_apply, det_apply, finset_sum_coeff]
refine Finset.sum_congr rfl ?_
simp only [Finset.mem_univ, forall_true_left]
intro g
convert coeff_smul (R := α) (sign g) _ _
rw [← mul_one (Fintype.card n)]
convert (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm
· simp [coeff_C]
· rintro p -
dsimp only [add_apply, smul_apply, map_apply, smul_eq_mul]
compute_degree
