coeff_det_X_add_C_zero — Mathlib

English

The constant term (coefficient of X^0) of det((X)·A.map C + B.map C) is det B.

Русский

Постоянный коэффициент детерминанта det((X)·A.map C + B.map C) равен det B.

LaTeX

$$$\\coeff\\big(\\det\\big((X : \\alpha[X]) \\cdot A.map C + B.map C\\big)\\big)_{0} = \\det B$$$

Lean4

theorem coeff_det_X_add_C_zero (A B : Matrix n n α) : coeff (det ((X : α[X]) • A.map C + B.map C)) 0 = det B :=
  by
  rw [det_apply, finset_sum_coeff, det_apply]
  refine Finset.sum_congr rfl ?_
  rintro g -
  convert coeff_smul (R := α) (sign g) _ 0
  rw [coeff_zero_prod]
  refine Finset.prod_congr rfl ?_
  simp

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