Commit 2020-10-17 18:26 edddb3b2
View on Github →feat(finsupp/basic): Add a variant of prod_map_domain_index for when f is injective (#4645)
This puts much weaker restrictions on h, making this easier to apply in some situations
feat(finsupp/basic): Add a variant of prod_map_domain_index for when f is injective (#4645)
This puts much weaker restrictions on h, making this easier to apply in some situations