Out of the last four definitions (MagmaHom.toMagmaEquiv), we don't want all of them.
Please tell me which one or two we should keep.

awaiting-review

I guess we should follow whatever Mathlib does for the analogous [Mul] and [Add] homomorphisms with regards to making equivalences.

By the way, if you could also update the top-level equational_theories.lean to include your new file, and also add a description of your file to the core lean files listed in CONTRIBUTING.md, that would be great.

You could add a poll to the zulip poll thread to see if there are any strong feelings on this issue

I will add more API tomorrow.

Actually with the likely refactor in which Magma may become closer to Mul this PR may become obsolete. Stay tuned...

There wasn't enough consensus to move from Magma to Mul, so I think we will go ahead with your PR after all. It looks like you selected a MagmaHom.toMagmaEquiv, so all we need to do now is fix the conflict with CONTRIBUTING.md and we are good to merge!

All right, the PR is ready for review now.