constantCoeff_C

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

For any a ∈ R, constantCoeff (C a) = a.

Русский

Для любого a ∈ R, постоянный коэффициент C a равен a.

LaTeX

$$$\operatorname{constantCoeff}(C a) = a$$$

Lean4

@[simp]
theorem constantCoeff_C (a : R) : constantCoeff (σ := σ) (C a) = a :=
  rfl

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

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

Разделы

Аффилиация

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