mathlib
edddb3b2 - feat(finsupp/basic): Add a variant of `prod_map_domain_index` for when f is injective (#4645)

Commit

5 years ago

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

References

#4925 - Make prime-avoidance branch build

Author

eric-wieser

Parents

85eb12df

mathlib edddb3b2 - feat(finsupp/basic): Add a variant of `prod_map_domain_index` for when f is injective (#4645)

mathlib
edddb3b2 - feat(finsupp/basic): Add a variant of `prod_map_domain_index` for when f is injective (#4645)