isWeightedHomogeneous_monomial — Mathlib

English

A monomial X^d with any coefficient r is weighted homogeneous of degree weight w d.

Русский

Моном X^d с коэффициентом r взвешенно однороден степени weight w d.

LaTeX

$$IsWeightedHomogeneous w (monomial d r) (weight w d)$$

Lean4

/-- Monomials are weighted homogeneous. -/
theorem isWeightedHomogeneous_monomial (w : σ → M) (d : σ →₀ ℕ) (r : R) {m : M} (hm : weight w d = m) :
    IsWeightedHomogeneous w (monomial d r) m := by
  classical
  intro c hc
  rw [coeff_monomial] at hc
  split_ifs at hc with h
  · subst c
    exact hm
  · contradiction

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