coeffs — Mathlib

English

The coefficients of the representation of h in the basis ε are given by h.coeffs m i = ε_i m for all m ∈ M and i ∈ ι.

Русский

Коэффициенты представления элемента m по базису ε заданы как h.coeffs m i = ε_i m для всех m ∈ M и i ∈ ι.

LaTeX

$$$ h.coeffs\\ m\\ i = \\varepsilon_i(m) $$$

Lean4

/-- The coefficients of `v` on the basis `e` -/
def coeffs (h : DualBases e ε) (m : M) : ι →₀ R where
  toFun i := ε i m
  support := (h.finite m).toFinset
  mem_support_toFun i := by rw [Set.Finite.mem_toFinset, Set.mem_setOf_eq]

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