coeff_ofFinsuppLinearMap — Mathlib

English

For f : Γ →₀ V and a ∈ Γ, the coefficient at a of the Hahn series image of f under ofFinsuppLinearMap is f(a).

Русский

Для f : Γ →₀ V и a ∈ Γ коэффициент при a у ряда Хана, полученного через ofFinsuppLinearMap, равен f(a).

LaTeX

$$$(\\text{ofFinsuppLinearMap } R\\, f).\\text{coeff} \\ a = f\\ a$$$

Lean4

@[simp]
theorem coeff_ofFinsuppLinearMap (f : Γ →₀ V) (a : Γ) : (ofFinsuppLinearMap R f).coeff a = f a :=
  rfl

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