[Merged by Bors] - chore(group_theory): some new convenience lemmas

[PatrickMassot]

from LTE

---

This does not decrease the mess with group_theory/coset vs group_theory/quotient_group and various implicit or explicit parameters, it's only adding more API on top of the mess. In particular I added ad hoc reformulations for additive groups in order to avoid the x + -y curse of to_additive.

I also changed slightly an old lemma since preimages are more convenient to use than direct images.

[eric-wieser]

I'm not really convinced that the mk'_eq_mk'_... lemmas here are a good idea. Why duplicate every lemma about coe when the user can just write rw coe_mk', the_rest_of_the_proof_using_coe?

[PatrickMassot]

I tried using only coe earlier but it was painful. I'll try again because I don't have time to waste on this discussion.

[eric-wieser]

Thanks for pruning those lemmas, the rest looks good to me (modulo a whitespace nit you can ignore).

This lemma might be worth adding just below inv_mem_iff in subgroup.lean too:

@[to_additive] lemma div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
by rw [←H.inv_mem_iff, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, inv_inv]

which gives you the additive add_subgroup.sub_mem_comm_iff : a - b ∈ H ↔ b - a ∈ H which it sounds like would make switching between the variations you had before easier.

[eric-wieser]

bors d+

[bors]

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

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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