monomial_zero_eq_C_apply

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

The action of monomial with index 0 on a is the same as applying C to a.

Русский

Действие мономиала с индексом 0 на a равно применению C к a.

LaTeX

$$$$ \operatorname{monomial}(0 : σ\to_0 ℕ) \, a = C(a) $$$$

Lean4

theorem monomial_zero_eq_C_apply (a : R) : monomial (0 : σ →₀ ℕ) a = C a :=
  rfl

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

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

Разделы

Аффилиация

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