English
A matrix polynomial equivalence shows that a matrix polynomial under expansion corresponds to X^k − C(M^k).
Русский
Эквивалентность матричного полинома говорит, что при расширении матричного полинома получаем X^k − C(M^k).
LaTeX
$$$$ \\text{matPolyEquiv}\\big( X^k, M^{k}\\big) = X^{k} - C\\big(M^{k}\\big). $$$$
Lean4
theorem matPolyEquiv_eq_X_pow_sub_C {K : Type*} (k : ℕ) [CommRing K] (M : Matrix n n K) :
matPolyEquiv ((expand K k : K[X] →+* K[X]).mapMatrix (charmatrix (M ^ k))) = X ^ k - C (M ^ k) :=
by
ext m i j
rw [coeff_sub, coeff_C, matPolyEquiv_coeff_apply, RingHom.mapMatrix_apply, Matrix.map_apply, AlgHom.coe_toRingHom,
DMatrix.sub_apply, coeff_X_pow]
by_cases hij : i = j
· rw [hij, charmatrix_apply_eq, map_sub, expand_C, expand_X, coeff_sub, coeff_X_pow, coeff_C]
split_ifs with mp m0 <;> simp
· rw [charmatrix_apply_ne _ _ _ hij, map_neg, expand_C, coeff_neg, coeff_C]
split_ifs with m0 mp <;> simp_all
