constantCoeff_comp_C

Mathlib.Algebra.MvPolynomial.Basic

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

English

The composition of constantCoeff with the constant map C gives the identity on R.

Русский

Состав constantCoeff с константной картой C даёт тождество на R.

LaTeX

$$$ constantCoeff.comp (C : R \\to+* MvPolynomial(\\sigma, R)) = \\mathrm{id} R $$$

Lean4

@[simp]
theorem constantCoeff_comp_C : constantCoeff.comp (C : R →+* MvPolynomial σ R) = RingHom.id R :=
  by
  ext x
  exact constantCoeff_C σ x

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

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

Разделы

Аффилиация

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