*): Add simps projections to many equivs and homs (#4818)

Commit

5 years ago

feat(data/equiv, algebra/*): Add simps projections to many equivs and homs (#4818) This doesn't actually change any existing lemmas to use these projections.

References

#4925 - Make prime-avoidance branch build

Author

eric-wieser

Parents

d46d0c27

mathlib 5ae192eb - feat(data/equiv, algebra/*): Add simps projections to many equivs and homs (#4818)

mathlib
5ae192eb - feat(data/equiv, algebra/*): Add simps projections to many equivs and homs (#4818)