Commit 2022-12-07 02:29 376d360e

feat: port Algebra.Group.Ext (#850) mathlib SHA: e574b1a4e891376b0ef974b926da39e05da12a06 Porting notes:

1. Constructing a MonoidHom (or OneHom) with ambiguous instances requires the use of the mk constructor and using (_) to disable the TC inference on the input type.
2. For the proofs of injectivity, I needed to destructure the instances further for the proofs to work. In the case of CancelCommMonoid.toCommMonoid_injective, I needed to nest injection tactics. Not sure if injection or congr should do these automatically.