[Merged by Bors] - feat: port GroupTheory/Submonoid/Basic

[ADedecker]

No description provided.

[ChrisHughes24]

bors d+

[bors]

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

[urkud]

• The loop in pow_mem can be resolved if you add : Prop to MulMemClass etc.
• eq_mlocus etc were there for submonoids so that we can use non-m versions for subgroups.

Please ping me on Zulip when this is ready for review again. I want to have another look before it's merged.

[urkud]

bors d-

[ADedecker]

The loop in pow_mem can be resolved if you add : Prop to MulMemClass etc.

That didn't make the situation better on my side 🤔
What did however was changing some arguments from [] to {} in SubmonoidClass.toOneMemClass

eq_mlocus etc were there for submonoids so that we can use non-m versions for subgroups.

Yes I know that, but I saw you removed some of them when porting GroupTheory.Subsemigroup.Basic. Is it because they weren't supposed to be there in the first place? Anyway, I'll add them back

[urkud]

eq_mlocus etc were there for submonoids so that we can use non-m versions for subgroups.

Yes I know that, but I saw you removed some of them when porting GroupTheory.Subsemigroup.Basic. Is it because they weren't supposed to be there in the first place? Anyway, I'll add them back

I think that somebody copied them from submonoid to subsemigroup in mathlib. IMHO, they shouldn't be there.

[urkud]

Thanks! I think that these typeclasses should be moved to Prop but this can wait for leanprover-community/mathlib#18015 to be merged.
bors d+

[bors]

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

[ADedecker]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[semorrison]

@ADedecker, @urkud, @ChrisHughes24, just a heads up that this PR has lots of missing #aligns for the to_additive versions of statements. We should be checking for this when reviewing.