IsHomogeneous — Mathlib

English

A multivariate polynomial is homogeneous of degree n if every monomial appearing in it has total degree n.

Русский

Многочлен с несколькими переменными однороден степени n, если каждая мономика, встречающаяся в нём, имеет общую степень n.

LaTeX

$$$\\text{IsHomogeneous}(\\varphi,n) \\iff \\text{all monomials in } \\varphi \\text{ have degree } n$$$

Lean4

/-- A multivariate polynomial `φ` is homogeneous of degree `n`
if all monomials occurring in `φ` have degree `n`. -/
def IsHomogeneous [CommSemiring R] (φ : MvPolynomial σ R) (n : ℕ) :=
  IsWeightedHomogeneous 1 φ n

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