Commit 2024-01-17 12:06 45df8238

chore: refactor of Algebra/Group/Defs to reduce imports (#9606) We are not that far from the point that Algebra/Group/Defs depends on nothing significant besides simps and to_additive. This removes from Mathlib.Algebra.Group.Defs the dependencies on

• Mathlib.Tactic.Basic (which is a grab-bag of random stuff)
• Mathlib.Init.Algebra.Classes (which is ancient and half-baked)
• Mathlib.Logic.Function.Basic (not particularly important, but it is barely used in this file) The goal is to avoid all unnecessary imports to set up the definitions of basic algebraic structures. We also separate out Mathlib.Tactic.TypeStar and Mathlib.Tactic.Lemma as prerequisites to Mathlib.Tactic.Basic, but which can be imported separately when the rest of Mathlib.Tactic.Basic is not needed.