mathlib3

0b966303 - feat(algebra/{monoid_algebra/basic,free_non_unital_non_assoc_algebra,lie/free}): generalize typeclasses (#11283)

feat(algebra/{monoid_algebra/basic,free_non_unital_non_assoc_algebra,lie/free}): generalize typeclasses (#11283) This fixes a number of missing or problematic typeclasses: * The smul typeclasses on `monoid_algebra` had overly strong assumptions * `add_comm_group (monoid_algebra k G)` was missing. * `monoid_algebra` had diamonds in its int-module structures, which were different between the one inferred from `ring` and `add_group`. * `monoid_algebra` was missing an instance of the new `non_unital_non_assoc_ring`. * `free_non_unital_non_assoc_algebra` was missing a lot of smul typeclasses and transitive module structures that it should inherit from `monoid_algebra`. Since every instance should just be inherited, we change `free_non_unital_non_assoc_algebra` to an abbreviation. * `free_lie_algebra` had diamonds in its int-module and nat-module structures. * `free_lie_algebra` was missing transitive module structures. This also golfs some proofs about `free_non_unital_non_assoc_algebra`, and removes the `irreducible` attributes since these just make some obvious proofs more awkward.