Commit 2023-02-03 16:27 207a0e5f

View on Github →

feat: Port/Data.Finsupp.ToDfinsupp (#1995) port of data.finsup.to_dfinsupp includes naming of instances in Data.Finsupp.Defs Had to unroll the instance defs for sigmaFinsuppLequivDfinsupp (duplicating defs) to address a timeout issue.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Created Mathlib/Data/Finsupp/ToDfinsupp.lean

added def Dfinsupp.toFinsupp

added theorem Dfinsupp.toFinsupp_add

added theorem Dfinsupp.toFinsupp_coe

added theorem Dfinsupp.toFinsupp_neg

added theorem Dfinsupp.toFinsupp_single

added theorem Dfinsupp.toFinsupp_smul

added theorem Dfinsupp.toFinsupp_sub

added theorem Dfinsupp.toFinsupp_support

added theorem Dfinsupp.toFinsupp_toDfinsupp

added theorem Dfinsupp.toFinsupp_zero

added def Finsupp.toDfinsupp

added theorem Finsupp.toDfinsupp_add

added theorem Finsupp.toDfinsupp_coe

added theorem Finsupp.toDfinsupp_neg

added theorem Finsupp.toDfinsupp_single

added theorem Finsupp.toDfinsupp_smul

added theorem Finsupp.toDfinsupp_sub

added theorem Finsupp.toDfinsupp_toFinsupp

added theorem Finsupp.toDfinsupp_zero

added def finsuppAddEquivDfinsupp

added def finsuppEquivDfinsupp

added def finsuppLequivDfinsupp

added theorem finsuppLequivDfinsupp_apply_apply

added theorem finsuppLequivDfinsupp_apply_toAddHom_apply

added theorem finsuppLequivDfinsupp_symmApply

added def sigmaFinsuppAddEquivDfinsupp

added def sigmaFinsuppEquivDfinsupp

added theorem sigmaFinsuppEquivDfinsupp_add

added theorem sigmaFinsuppEquivDfinsupp_apply

added theorem sigmaFinsuppEquivDfinsupp_single

added theorem sigmaFinsuppEquivDfinsupp_smul

added theorem sigmaFinsuppEquivDfinsupp_support

added theorem sigmaFinsuppEquivDfinsupp_symm_apply

added def sigmaFinsuppLequivDfinsupp

added theorem toDfinsupp_support