matPolyEquiv_coeff_apply_aux_2 — Mathlib

English

Another coefficient-level identity: coefficient extraction commutes with matPolyEquiv on single-entry polynomials.

Русский

Еще одно тождество на уровне коэффициентов: извлечение коэффициентов латентно совпадает через matPolyEquiv на единичных полиномах.

LaTeX

$$$\\text{coeff}(\\text{matPolyEquiv}(\\text{single } i j \\lvert\\!\\text{ monomial } k x), k) = \\text{single } i j (\\text{coeff } p k)$$$

Lean4

theorem matPolyEquiv_coeff_apply_aux_2 (i j : n) (p : R[X]) (k : ℕ) :
    coeff (matPolyEquiv (single i j p)) k = single i j (coeff p k) :=
  by
  refine Polynomial.induction_on' p ?_ ?_
  · intro p q hp hq
    ext
    simp [hp, hq, coeff_add, add_apply, single_add]
  · intro k x
    simp only [matPolyEquiv_coeff_apply_aux_1, coeff_monomial]
    split_ifs <;>
      · funext
        simp

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