mathlib

99130d84 - chore(algebra/monoid_algebra): Reorder lemmas, name some sections for clarity (#4535)

chore(algebra/monoid_algebra): Reorder lemmas, name some sections for clarity (#4535) This also reduces the scope of `local attribute [reducible] add_monoid_algebra` to the sections which actually need it.