constantCoeff_smul

Mathlib.Algebra.MvPolynomial.Basic

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

← MathLib Explorer

English

The composition of constantCoeff with C equals the identity on R.

Русский

Составление constantCoeff с C дает тождество на R.

LaTeX

$$$ constantCoeff \\circ C = \\mathrm{id}_{R}. $$$

Lean4

@[simp]
theorem constantCoeff_smul {R : Type*} [SMulZeroClass R S₁] (a : R) (f : MvPolynomial σ S₁) :
    constantCoeff (a • f) = a • constantCoeff f :=
  rfl

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

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

Разделы

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

Аффилиация

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