equivFunOnFinite_symm_eq_sum — Mathlib

English

The inverse of a finite-equivalence equals the finite sum of basis functions.

Русский

Обратное к эквививалентности на конечном множестве равно квантованию по базисам.

LaTeX

$$$$ \mathrm{equivFunOnFinite}.\mathrm{symm} f = \sum_{a} \mathrm{single}_a (f(a)). $$$$

Lean4

theorem equivFunOnFinite_symm_eq_sum [Fintype α] [AddCommMonoid M] (f : α → M) :
    equivFunOnFinite.symm f = ∑ a, Finsupp.single a (f a) :=
  by
  rw [← univ_sum_single (equivFunOnFinite.symm f)]
  ext
  simp

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