Commit 2021-08-09 10:27 67282017
View on Github →chore(data/finsupp): add missing lemmas (#8553)
These lemmas are needed by [simps {simp_rhs := tt}] when composing equivs, otherwise simp doesn't make progress on (map_range.add_equiv f).to_equiv.symm x which should simplify to map_range f.to_equiv.symm x.