Commit 2020-10-03 23:52 333c2164

chore(algebra/group/type_tags): Use ≃ instead of → (#4346) These functions are all equivalences, so we may as well expose that in their type This also fills in some conversions that were missing. Unfortunately this requires some type ascriptions in a handful of places. It might be possible to remove these somehow. This zulip thread contains a mwe: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Type.20inference.20on.20.60.E2.86.92.60.20vs.20.60.E2.89.83.60/near/211922501.