English
For a square matrix M, the matPolyEquiv of its charmatrix equals X minus CM, where CM is the matrix obtained by embedding M into polynomials as constants.
Русский
Для квадратной матрицы M матрично-полиноминальная эквивалентность charmatrix эквивалентна X минус CM, где CM — это матрица, полученная из M путём вложения его элементов как констант в многочлены.
LaTeX
$$$\operatorname{matPolyEquiv}\bigl(\operatorname{charmatrix}(M)\bigr) = X - C M$$$
Lean4
theorem matPolyEquiv_charmatrix : matPolyEquiv (charmatrix M) = X - C M :=
by
ext k i j
simp only [matPolyEquiv_coeff_apply, coeff_sub]
by_cases h : i = j
· subst h
rw [charmatrix_apply_eq, coeff_sub]
simp only [coeff_X, coeff_C]
split_ifs <;> simp
· rw [charmatrix_apply_ne _ _ _ h, coeff_X, coeff_neg, coeff_C, coeff_C]
split_ifs <;> simp [h]
