matPolyEquiv_symm_apply_coeff — Mathlib

English

For p a matrix of polynomials, the coefficient at position i,j,k of matPolyEquiv.symm p equals the coefficient k of p at i,j.

Русский

Для p — матрица полиномов, коэффициент k в позиции i,j после применения symm равен коэффициенту k в p на позиции i,j.

LaTeX

$$$\\text{coeff}(\\text{matPolyEquiv}.\\mathrm{symm}\\ p\\ i\\ j)\\ k = \\text{coeff}\\ p\\ k\\ i\\ j$$$

Lean4

@[simp]
theorem matPolyEquiv_symm_apply_coeff (p : (Matrix n n R)[X]) (i j : n) (k : ℕ) :
    coeff (matPolyEquiv.symm p i j) k = coeff p k i j :=
  by
  have t : p = matPolyEquiv (matPolyEquiv.symm p) := by simp
  conv_rhs => rw [t]
  simp only [matPolyEquiv_coeff_apply]

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