constantCoeff_comp_C

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

The composition of constantCoeff with C equals the identity on R: constantCoeff ∘ C = id.

Русский

Составление constantCoeff с C даёт тождественную отображение на R: constantCoeff ∘ C = id.

LaTeX

$$$\bigl$constantCoeff \circ C = \mathrm{id} \bigr$$$

Lean4

@[simp]
theorem constantCoeff_comp_C : (constantCoeff (σ := σ)).comp C = RingHom.id R :=
  rfl

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

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

Разделы

Аффилиация

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