Commit 2022-10-14 00:13 26e9fca1

feat: replace Algebra/Group/{Defs,Basic} with direct ports from mathlib3 (#457) This PR discards and replaces with a direct port from mathlib3 the files:

• Algebra/Group/Defs.lean
• Algebra/Group/Basic.lean These files contained an ad-hoc redevelopment of parts of the algebraic hierarchy, and the expense of interfacing their content with other material which we need to port from mathlib3 to support tactic development was too high. The rest of the PR consists of making everything work again! To do so, we add partial ports of mathlib3's
• Algebra/Group/Units.lean
• Algebra/Group/Semiconj.lean
• Algebra/Group/Commute.lean (just the initial segment of each which was required to provide the lemmas we need to patch up problems from the main replacement above). Unfortunately it's still not working: there are mysterious (to me!) failures in Tactic/Ring.lean, which all seem to come down to the simplifier not wanting to use zero_add and add_zero, even though exact or rw accepts them. If @digama0 or @gebner would be able to have a look at these and provide some advice I'd much appreciate it.

• depends on: #461