coeff_comp_monomial

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

The composition coeff(n) ∘ monomial(n) is the identity on R.

Русский

Состав коэффициента и монома для одного и того же индекса равен единице на R.

LaTeX

$$$(\\mathrm{coeff}(n) \\circ \\mathrm{monomial}(n)) = \\mathrm{id}$$$

Lean4

@[simp]
theorem coeff_comp_monomial (n : σ →₀ ℕ) : (coeff (R := R) n).comp (monomial n) = LinearMap.id :=
  LinearMap.ext <| coeff_monomial_same n

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

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

Разделы

Аффилиация

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