support_subset_support_matPolyEquiv

English

For any matrix m with entries in R[X], the support of each entry m_{i j} is contained in the support of matPolyEquiv m.

Русский

Для любой матрицы m с элементами в R[X] множества поддержки каждого элемента m_{i j} вложены в множество поддержки матPolyEquiv m.

LaTeX

$$$\\mathrm{supp}(m_{i j}) \\subseteq \\mathrm{supp}(\\mathrm{matPolyEquiv}\, m)$$$

Lean4

theorem support_subset_support_matPolyEquiv (m : Matrix n n R[X]) (i j : n) :
    support (m i j) ⊆ support (matPolyEquiv m) := by
  intro k
  contrapose
  simp only [notMem_support_iff]
  intro hk
  rw [← matPolyEquiv_coeff_apply, hk, zero_apply]

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