[Merged by Bors] - fix(algebra/ring/basic): delete mul_self_sub_mul_self_eq

[bryangingechen]

It's redundant with mul_self_sub_mul_self.

Also renamed mul_self_sub_one_eq to mul_self_sub_one.

---

Zulip thread.

[bryangingechen]

Oh, I just realized that the names are inconsistent when it comes to whether they should end in eq:

We have:

• mul_self_sub_one_eq
• nat.mul_self_sub_mul_self_eq

We also have:

• pow_two_sub_pow_two

And this PR keeps mul_self_sub_mul_self.

My (slight) preference is to remove the eqs from all these.

[jcommelin]

I agree that we can drop those _eq suffixes. Do you want to do that in this PR?

[semorrison]

I'll leave it to you to merge after deciding what to do with the names.

bors d+

[bors]

✌️ bryangingechen can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bryangingechen]

I agree that we can drop those _eq suffixes. Do you want to do that in this PR?

Ha, I just realized that nat.mul_self_sub_mul_self_eq is defined in core so I unfortunately can't change the name here. I did change mul_self_sub_one_eq to mul_self_sub_one though.

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests