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]