Commit 2020-10-05 11:38 b44e927e
View on Github →feat(data/finsupp): Make finsupp.dom_congr a ≃+ (#4398)
Since this has additional structure, it may as well be part of the type
feat(data/finsupp): Make finsupp.dom_congr a ≃+ (#4398)
Since this has additional structure, it may as well be part of the type