English
If a k-th coefficient of polyCharpoly φ b vanishes for a basis b, then the k-th coefficient of polyCharpoly φ b' vanishes for any other basis b'.
Русский
Если коэффициент k полинома polyCharpoly φ b равен нулю для базиса b, то коэффициент k того же полинома для другого базиса b' также равен нулю.
LaTeX
$$$((\mathrm{polyCharpoly}\ φ\ b).\mathrm{coeff} k) = 0 \Rightarrow ((\mathrm{polyCharpoly}\ φ\ b').\mathrm{coeff} k) = 0$$$
Lean4
theorem polyCharpoly_coeff_eq_zero_of_basis (b : Basis ι R L) (b' : Basis ι' R L) (k : ℕ)
(H : (polyCharpoly φ b).coeff k = 0) : (polyCharpoly φ b').coeff k = 0 :=
by
rw [polyCharpoly, polyCharpolyAux, Polynomial.coeff_map] at H ⊢
set B := (Module.Free.chooseBasis R M).end
set g := toMvPolynomial b' b LinearMap.id
apply_fun (MvPolynomial.bind₁ g) at H
have : toMvPolynomial b' B φ = fun i ↦ (MvPolynomial.bind₁ g) (toMvPolynomial b B φ i) :=
funext <| toMvPolynomial_comp b' b B φ LinearMap.id
rwa [map_zero, RingHom.coe_coe, MvPolynomial.bind₁_bind₁, ← this] at H
