homogeneousComponent_isHomogeneous

Mathlib.RingTheory.MvPolynomial.Homogeneous

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

English

For any φ, the degree-n component homogeneousComponent(n) φ is homogeneous of degree n.

Русский

Компонента по степени n параграфа φ является однородной по степени n.

LaTeX

$$(homogeneousComponent(n)\\;φ).IsHomogeneous n$$

Lean4

theorem homogeneousComponent_isHomogeneous : (homogeneousComponent n φ).IsHomogeneous n :=
  weightedHomogeneousComponent_isWeightedHomogeneous n φ

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

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

Разделы

Аффилиация

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