matPolyEquiv_coeff_apply — Mathlib

English

Same auxiliary lemma as above, presented for a distinct instance.

Русский

Та же вспомогательная лемма, приведенная для другого примера.

LaTeX

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

Lean4

@[simp]
theorem matPolyEquiv_coeff_apply (m : Matrix n n R[X]) (k : ℕ) (i j : n) :
    coeff (matPolyEquiv m) k i j = coeff (m i j) k :=
  by
  refine Matrix.induction_on' m ?_ ?_ ?_
  · simp
  · intro p q hp hq
    simp [hp, hq]
  · intro i' j' x
    rw [matPolyEquiv_coeff_apply_aux_2]
    dsimp [single]
    split_ifs <;> rename_i h
    · constructor
    · simp

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