mathlib3
b44e927e - feat(data/finsupp): Make `finsupp.dom_congr` a `≃+` (#4398)

Commit

5 years ago

feat(data/finsupp): Make `finsupp.dom_congr` a `≃+` (#4398) Since this has additional structure, it may as well be part of the type

References

Author

eric-wieser

Parents