isHomogeneous_monomial — Mathlib

English

For a monomial determined by a finite support d, the polynomial c·monomial(d) is homogeneous of degree d.degree.

Русский

Для монома, задаваемого поддержкой d, полином c·monomial(d) однороден степени d.degree.

LaTeX

$$$\\text{IsHomogeneous}( \\mathrm{monomial}(d), d.\\deg )$$$

Lean4

theorem isHomogeneous_monomial {d : σ →₀ ℕ} (r : R) {n : ℕ} (hn : d.degree = n) : IsHomogeneous (monomial d r) n :=
  by
  rw [degree_eq_weight_one] at hn
  exact isWeightedHomogeneous_monomial 1 d r hn

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