IsWeightedHomogeneous

Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

URI: https://scilib.ai/kg/mathlib#MvPolynomial.IsWeightedHomogeneous

Lean4

/-- A multivariate polynomial `φ` is weighted homogeneous of weighted degree `m` if all monomials
  occurring in `φ` have weighted degree `m`. -/
def IsWeightedHomogeneous (w : σ → M) (φ : MvPolynomial σ R) (m : M) : Prop :=
  ∀ ⦃d⦄, coeff d φ ≠ 0 → weight w d = m

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru