monomial_eq_mk

Mathlib.RingTheory.PowerSeries.Basic

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

English

The monomial n a equals mk of the function f with f(m) = a if m = n, else 0.

Русский

Моном n a равен mk функции f, где f(m) = a, если m = n, иначе 0.

LaTeX

$$$$ \operatorname{monomial}(n,a) = \mathrm{mk}\left(\lambda m. \begin{cases} a & m = n \\ 0 & m \neq n \end{cases}\right) $$$$

Lean4

theorem monomial_eq_mk (n : ℕ) (a : R) : monomial n a = mk fun m => if m = n then a else 0 :=
  ext fun m => by rw [coeff_monomial, coeff_mk]

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

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

Разделы

Аффилиация

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