Commit 2022-01-26 17:10 8fbc009a

View on Github →

feat(data/{dfinsupp,finsupp}/basic): fun_like instances for Π₀ i, α i and ι →₀ α (#11667) This provides the fun_like instances for finsupp and dfinsupp and deprecates the lemmas that are now provided by the fun_like API.

Estimated changes

Modified src/data/dfinsupp/basic.lean

modified theorem dfinsupp.coe_fn_injective

modified theorem dfinsupp.ext

modified theorem dfinsupp.ext_iff

Modified src/data/finsupp/basic.lean

modified theorem finsupp.coe_fn_inj

modified theorem finsupp.coe_fn_injective

modified theorem finsupp.congr_fun

modified theorem finsupp.ext

modified theorem finsupp.ext_iff