Commit 2022-02-10 20:43 09293874

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.