of_coeff_apply_coeff — Mathlib

English

For every f and hf, the coefficient n of the Hahn-module realization of the constructed coefficient operator applied to x equals f(n) x.

Русский

Для любых f и hf коэффициент n представления на основе Hahn-модуля сконструированного коэффициентного оператора, применённого к x, равен f(n) x.

LaTeX

$$$\\operatorname{coeff}_n\\big((\\mathrm{of\\_coeff}\\ f\\ hf)\\ x\\big) = (f(n))x$$$

Lean4

@[simp]
theorem of_coeff_apply_coeff (f : ℤ → Module.End R V) (hf : ∀ (x : V), ∃ n, ∀ m < n, (f m) x = 0) (x : V) (n : ℤ) :
    ((HahnModule.of R).symm ((of_coeff f hf) x)).coeff n = (f n) x := by rfl

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