Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sigma_finsupp_equiv_dfinsupp_single

Modification history

2023-01-23 10:09
src/data/finsupp/to_dfinsupp.lean
fix(*/finsupp/*): add missing decidable arguments in lemma statements (#18251) …
Modified sigma_finsupp_equiv_dfinsupp_singleView on Github →
2021-11-13 02:46
src/data/finsupp/to_dfinsupp.lean
feat(analysis/inner_product_space/projection): orthonormal basis subordinate to an `orthogonal_family` (#10208) …
Added sigma_finsupp_equiv_dfinsupp_singleView on Github →