totalDegree_le — Mathlib

English

If φ is homogeneous of degree n, then the total degree of φ is at most n.

Русский

Если φ однороден степени n, то общая степень φ не превосходит n.

LaTeX

$$IsHomogeneous(φ, n) → φ.totalDegree ≤ n$$

Lean4

/-- The homogeneous degree bounds the total degree.

See also `MvPolynomial.IsHomogeneous.totalDegree` when `φ` is non-zero. -/
theorem totalDegree_le (hφ : IsHomogeneous φ n) : φ.totalDegree ≤ n :=
  by
  apply Finset.sup_le
  intro d hd
  rw [mem_support_iff] at hd
  simp_rw [Finsupp.sum, ← hφ hd, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum, le_rfl]

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