mathlib

09293874 - feat(group_theory/group_action/defs): add ext attributes (#11936)

feat(group_theory/group_action/defs): add ext attributes (#11936) This adds `ext` attributes to `has_scalar`, `mul_action`, `distrib_mul_action`, `mul_distrib_mul_action`, and `module`. The `ext` and `ext_iff` lemmas were eventually generated by `category_theory/preadditive/schur.lean` anyway - we may as well generate them much earlier. The generated lemmas are slightly uglier than the `module_ext` we already have, but it doesn't really seem worth the trouble of writing out the "nice" versions when the `ext` tactic cleans up the mess for us anyway.