isHomogeneous_C_mul_X

Mathlib.RingTheory.MvPolynomial.Homogeneous

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

English

The monomial X_i^n is homogeneous of degree n.

Русский

Моном X_i^n однороден степени n.

LaTeX

$$IsHomogeneous(X_i^n, n)$$

Lean4

theorem _root_.MvPolynomial.isHomogeneous_C_mul_X (r : R) (i : σ) : (C r * X i).IsHomogeneous 1 :=
  (isHomogeneous_X _ _).C_mul _

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

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

Разделы

Аффилиация

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