feat(data/equiv/algebra): add add_equiv and mul_equiv

[kbuzzard]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[kbuzzard]

I needed these for the perfectoid project; basically I did what I needed, but it seemed comparable with what had been done for ring_equiv.

[jcommelin]

How long will it take before we also need add_monoid_equiv and add_group_equiv and then we don't have subscript letters for those...

[ChrisHughes24]

How long will it take before we also need add_monoid_equiv and add_group_equiv and then we don't have subscript letters for those...

I think it would be good if is_group_hom := is_monoid_hom and group_equiv := monoid_equiv. Then we could use notation like ≃+ and ≃* I guess.

[ChrisHughes24]

In fact, it turns out that for surjective functions, you don't need the map_one axiom for a monoid hom, so we could just do add preserving equivs and mul preserving equivs.

[kbuzzard]

I've now switched to mul_equiv, which is an equiv of types with has_mul, with the equiv preserving the multiplication. This means that one no longer needs monoid_equiv or group_equiv because they both turn out to be special cases of mul_equiv. I added add_equiv for good measure.

[ChrisHughes24]

It would be good to have to_additive attributes everywhere.

[kbuzzard]

It would be good to have to_additive attributes everywhere.

I have added them to everything I added, and to some stuff which other people have added too (now I understand how it all works)