monomial_zero_eq_C

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

The monomial of index 0 with coefficient a acts as the image of a under the canonical embedding C.

Русский

Мономиал с индексом 0 и коэффициентом a равен образу a через отображение C.

LaTeX

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

Lean4

@[simp]
theorem monomial_zero_eq_C : ⇑(monomial (R := R) (0 : σ →₀ ℕ)) = C :=
  rfl

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

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

Разделы

Аффилиация

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