Commit 2022-01-06 19:34 0b966303

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.