[Merged by Bors] - refactor(algebra/group/basic): rework lemmas on inv and neg

[MichaelStollBayreuth]

This PR adds the following lemma (and its additive equivalent).

theorem inv_eq_iff_eq_inv : a⁻¹ = b ↔ a = b⁻¹

and removes eq_inv_of_eq_inv, eq_inv_iff_eq_inv and inv_eq_iff_inv_eq (and their additive equivalents).

---

Note: As several files that are touched by this PR have already been ported to mathlib4, this needs a parallel mathlib4 PR.
I'll try to do that eventually, but if somebody else wants to go ahead with this, they are very welcome!

[eric-wieser]

Note: As the file that is touched by this PR has already been ported to mathlib4, this needs a parallel mathlib4 PR.
I'll try to do that soon, but if somebody else wants to go ahead with this, they are very wecome!

You don't need to actually put anything in the PR, just create a blank PR with a todo comment. You can then make the mathlib4 PR properly once this is merged and mathport has done the work for you.

[MichaelStollBayreuth]

Thanks for reminding me. As I don't think this has high priority, my current plan is to wait until the teaching period here is over (mid-February). Then I will have more time for Lean-related things; in particular, I plan to familiarize myself with Lean 4, and dealing with the corresponding PR for mathlib4 will be a good opportunity to get started.

(But if somebody else wants to go ahead with this, feel free to do so.)

[YaelDillies]

Why do you need this given that we have inv_eq_iff_inv_eq?

[MichaelStollBayreuth]

Because inv_eq_iff_inv_eq swaps the sides of the equality (so you'd need an additional eq_comm to rewrite).

[YaelDillies]

Would you mind changing inv_eq_iff_inv_eq instead, then? We don't need both lemmas, and we don't need the one-way implications either.

[eric-wieser]

I agree that the existing lemma swapping the sides is annoying; as @YaelDillies says, probably just replacing it with one that doesn't is a good move.

[MichaelStollBayreuth]

inv_eq_iff_inv_eq is used one time each in seven different files, two of which are already ported (algebra.group_with_zero.basic and data.set.pointwise.interval), one is in the process of being ported (data.real.conjugate_exponents, !4#2411) and the remaining four are not yet ported (data.real.golden_ratio, field_theory.finite.basic, ring_theory.algebraic, ring_theory.valuation.valuation_subring).

It looks like in most cases, proofs would simplify slightly when changing the statement as suggested (and in the other cases, there would be no change), so it certainly would make sense to just replace inv_eq_iff_inv_eq by inv_eq_iff_eq_inv.

On the other hand, this would make the whole thing quite a bit more involved (touching eight files instead of one, some of which are ported and some not). So my feeling is that it is perhaps better to do this after the port, in particular as there is no urgency whatsoever attached to this change.

[YaelDillies]

If only 2-3 files are touched by the port, and they all involve only trivial rewriting of existing proofs, I think that's alright.

[MichaelStollBayreuth]

and we don't need the one-way implications either.

Right now, there is a one-way implications with swapped sides (eq_inv_of_eq_inv), which is used to prove the iff versions eq_inv_iff_eq_inv and inv_eq_iff_inv_eq. (This seems to be the only use of it in mathlib, though.)

So, just to make sure I understand correctly what the suggestion is:

• remove eq_inv_of_eq_inv, eq_inv_iff_eq_inv and inv_eq_iff_inv_eq
• add inv_eq_iff_eq_inv (without a one-way version) + deal with the downstream effects

[MichaelStollBayreuth]

(I just realized there are two versions of the iff statement with swapped sides of the equality. One is used twice in ring_theory.valuation.basic and the other one is used once each in seven other files.)

[YaelDillies]

Ahah! I knew it was there somewhere. Up to you on whether you want to uniformise the API.

[MichaelStollBayreuth]

I just noticed that the additive versions of the two lemmas occur even more often... (including four occurrences of the one-way version).

• eq_neg_of_eq_neg occurs in data.int.basic (twice), linear_algebra.dimension and number_theory.modular
• eq_neg_iff_eq_neg occurs in algebra.periodic (twice), algebra.order.to_interval_mod, algebra.order.group.abs, algebraic_geometry.elliptic_curve.point, analysis.normed.group.quotient, analysis.special_functions.log.basic, analysis.special_functions.trigonometric.angle, data.polynomial.mirror and number_theory.legendre_symbol.quadratic_reciprocity
• neg_eq_iff_neg_eq occurs in algebra.order.group.abs, analysis.special_functions.gamma, data.num_lemmas, data.real.ereal (three times), data.real.golden_ratio, geometry.euclidean.angle.oriented.basic (twice), geometry.euclidean.angle.oriented.rotation, linear_algebra.affine_space.midpoint, linear_algebra.clifford_algebra.even_equiv, measure_theory.integral.divergence_theorem, number_theory.bernoulli, probability.martingale.borel_cantelli, ring_theory.int.basic, ring_theory.witt_vector.frobenius and set_theory.game.pgame

So this would touch more than 30 files in the end.
I think I'm close to the point where I wish I wouldn't have started this 😄

Do you still think it makes sense to do this now?

[YaelDillies]

Up to you, really! I think touching 30 files isn't so bad, but also I don't know how many are ported already.

[MichaelStollBayreuth]

OK, I have now made the change (including all necessary changes downstream).
So far, I don't think I'm up to dealing with the mathlib4 side of this (right now, there seem to be six files touched that are already ported). So if someone would like to do that, they are welcome.

[eric-wieser]

This looks great to me, thanks for pushing through with it.

[YaelDillies]

Thanks for powering through!

[eric-wieser]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests