coeff_mk

Mathlib.RingTheory.Perfection

URI: https://scilib.ai/kg/mathlib#Perfection.coeff_mk

English

@[simp] coeff-mk reduces to evaluating the underlying function: coeff(R,p,n) ⟨f,hf⟩ = f(n).

Русский

@[simp] coeff-mk сводится к вычислению базовой функции: coeff(R,p,n) ⟨f,hf⟩ = f(n).

LaTeX

$$coeff(R,p,n) ⟨f,hf⟩ = f(n)$$

Lean4

@[simp]
theorem coeff_mk (f : ℕ → R) (hf) (n : ℕ) : coeff R p n ⟨f, hf⟩ = f n :=
  rfl

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

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

Разделы

Аффилиация

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