Commit 2022-11-20 07:08 b73d5acd

feat: port remaining missing Algebra.GroupWithZero.Defs (#563) 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.