coeff_monomial_same

Mathlib.RingTheory.PowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#PowerSeries.coeff_monomial_same

English

For any n and a, the nth coefficient of the monomial with index n and value a is a.

Русский

Для любых n и a коэффициент n монома с индексом n равен a.

LaTeX

$$$$ \operatorname{coeff}_n(\operatorname{monomial}(n,a)) = a $$$$

Lean4

@[simp]
theorem coeff_monomial_same (n : ℕ) (a : R) : coeff n (monomial n a) = a :=
  MvPowerSeries.coeff_monomial_same _ _

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

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

Разделы

Аффилиация

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