[Merged by Bors] - feat: port remaining missing Algebra.GroupWithZero.Defs

[pechersky]

Tracking mathlib3 sha: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

The file had been missing some classes, added those.
Apart from adding missing classes, put in docstrings for the module, as well as classes and lemmas that were missing them.
Turns out this file doesn't rely on the Logic.Nontrivial import.
This file still has AddMonoidWithOne at the bottom of the file -- this is in dat.nat.cast.defs in mathlib3 -- I left it in because it is likely in this file to assist with downstream tactic usage.

[semorrison]

I don't understand what you mean by

Along with module, class, and some lemma docstrings
I kept the additional later-file defns near the bottom

[pechersky]

I tried to clarify the PR description.

[semorrison]

Hmm, I don't like this. When it's time to port this file, we should be completely replacing its contents with a one-to-one port of the mathlib3 file.

If there's "junk" in here from previous ad-hoc porting, that is still necessary on a temporary basis, lets move it out to a new file, possibly with some alarming name like Mathlib/Temporary/Algebra/GroupWithZero/Defs.lean...?

[pechersky]

Makes sense to me. Can we just port data.nat.cast.defs to not have to do a three-body problem?

[j-loreaux]

I have created #641 to port Mathlib.Data.Nat.Cast.Defs. That PR moves the AddMonoidWithOne and related lemmas out of this file (but leaves AddGroupWithOne for now because that belongs in Mathlib.Data.Int.Cast.Defs). The changes were significant enough that I thought it should have it's own PR instead of incorporating the changes here. So you may want to make this depends on that.

[j-loreaux]

It looks like data.int.cast.defs is only waiting on data.nat.cast.defs, so I'll just do that now and see if I can make it into one PR.

[semorrison]

@pechersky, could you work out how to merge master on this one?

[semorrison]

There was a bunch more that still needed porting, so I added that. Fortunately it was trivial.

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style