Commit 2024-02-06 15:01 ebb7343e

chore: Make sure WithOne doesn't import rings (#10275) Reorder the WithOne material.

• Algebra.Group.WithOne.Defs was hiding a Ring import! I credit Johan and Mario for https://github.com/leanprover-community/mathlib/pull/2707.
• WithBot is not needed to define WithOne.unone. It's simpler to redefine it by hand. In the future, we might want to have an Option version (but not sure how much that's worth, since it would basically be Option.get again).