smul_coeff_charpoly — Mathlib

English

The scalar action distributes to the coefficients of the charpoly.

Русский

Действие скаляра распределяется по коэффициентам характеристического многочлена.

LaTeX

$$$g \cdot (\text{charpoly}(b))_{n} = (\text{charpoly}(b))_{n}$ for all n.$$

Lean4

theorem smul_coeff_charpoly (b : B) (n : ℕ) (g : G) : g • (charpoly G b).coeff n = (charpoly G b).coeff n := by
  rw [← coeff_smul, smul_charpoly]

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