toMvPolynomial_isHomogeneous — Mathlib

English

For every i, the polynomial M.toMvPolynomial i is homogeneous of degree 1: all its monomials have total degree 1.

Русский

Для каждого i полином M.toMvPolynomial i однороден степени 1: все мономы имеют суммарную степень 1.

LaTeX

$$(M.toMvPolynomial i).IsHomogeneous 1$$

Lean4

theorem toMvPolynomial_isHomogeneous (M : Matrix m n R) (i : m) : (M.toMvPolynomial i).IsHomogeneous 1 :=
  by
  apply MvPolynomial.IsHomogeneous.sum
  rintro j -
  apply MvPolynomial.isHomogeneous_monomial _ _
  simp [Finsupp.degree, Finsupp.support_single_ne_zero _ one_ne_zero, Finset.sum_singleton, Finsupp.single_eq_same]

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