mathlib

f6f810cf - doc(algebraic_hierarchy): advice for adding new typeclasses (#6854)

doc(algebraic_hierarchy): advice for adding new typeclasses (#6854) This is not intended as document describing all the design decisions behind our algebraic hierarchy, but rather some advice for contributors adding new typeclasses. It can hopefully serve as a checklist for instances and definitions that should be made for any new algebraic structure being added to mathlib. Please edit as you see fit, contribute new sections, etc. I haven't written anything yet about interactions with topology or order structures. Please consider this an invitation, or otherwise we can delete those headings later. Thanks to @eric-wieser for providing the list of instances needed for each typeclass! Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>