linearCombination_eq_fintype_linearCombination

English

Yet another restatement of the finite-index equivalence between linearCombination and Fintype representations.

Русский

Ещё одна формулировка эквивалентности для конечного индекса между linearCombination и Fintype-вариантами.

LaTeX

$$$\\operatorname{linearCombination}_R v = \\operatorname{Fintype.linearCombination}_R v \\circ (\\mathrm{Finsupp.linearEquivFunOnFinite}_R^R \\alpha)^{-1}$$$

Lean4

theorem linearCombination_eq_fintype_linearCombination :
    (linearCombination R v).comp (Finsupp.linearEquivFunOnFinite R R α).symm.toLinearMap =
      Fintype.linearCombination R v :=
  LinearMap.ext <| linearCombination_eq_fintype_linearCombination_apply R v

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