isWeightedHomogeneous_X — Mathlib

English

An indeterminate X_i is weighted homogeneous of degree w(i).

Русский

Ввод X_i взвешенно однороден степени w(i).

LaTeX

$$IsWeightedHomogeneous w (X i) (w i)$$

Lean4

/-- An indeterminate `i : σ` is weighted homogeneous of degree `w i`. -/
theorem isWeightedHomogeneous_X (w : σ → M) (i : σ) : IsWeightedHomogeneous w (X i : MvPolynomial σ R) (w i) :=
  by
  apply isWeightedHomogeneous_monomial
  simp only [weight, LinearMap.toAddMonoidHom_coe, linearCombination_single, one_nsmul]

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