mathlib

461afdac - refactor(algebra/graded_monoid): provide better names for lemmas about internal graduations (#15488)

refactor(algebra/graded_monoid): provide better names for lemmas about internal graduations (#15488) This provides `set_like.one_mem_graded` as the preferred spelling of the projection `set_like.has_graded_one.one_mem`. This follows the usual pattern of not including the typeclass name in the lemma that it provides; we don't usually write `add_semigroup.add_assoc`. The new lemmas are now listed in the docstring as the preferred API for working with these typeclasses.