isHomogeneous_C

Mathlib.RingTheory.MvPolynomial.Homogeneous

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

← MathLib Explorer

English

The constant polynomial 1 is homogeneous of degree 0.

Русский

Константный полином 1 однороден степени 0.

LaTeX

$$$\\text{IsHomogeneous}(1,0)$$$

Lean4

theorem isHomogeneous_C (r : R) : IsHomogeneous (C r : MvPolynomial σ R) 0 :=
  by
  apply isHomogeneous_monomial
  simp only [Finsupp.degree, Finsupp.zero_apply, Finset.sum_const_zero]

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

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

Разделы

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

Аффилиация

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