mathlib

8f66240c - feat(group_theory/group_action): define `distrib_smul` and `smul_zero_class` (#16123)

feat(group_theory/group_action): define `distrib_smul` and `smul_zero_class` (#16123) These are two new superclasses of `distrib_mul_action` that get rid of the `mul_action` part: * `smul_zero_class` is `has_smul` + `a • 0 = 0` * `distrib_smul` is `smul_zero_class` + `a • (x + y) = a • x + a • y`. The motivation for these classes is to instantiate `qsmul` on `splitting_field`: in general scalar multiplication with rational numbers is not a `distrib_mul_action` but it is a `distrib_smul`, and `distrib_smul` is sufficient to lift an action to the `splitting_field`. I set up both `distrib_mul_action` and `smul_with_zero` to be subclasses of the above classes, and unify `smul_zero` (depending on `distrib_mul_action`) and `smul_zero'` (depending on `smul_with_zero`) into one lemma. There are a few places where I need to help the elaborator because e.g. it's expecting `units.mk0 a ha • 0 = 0` (with `smul` coming from `distrib_mul_action`) and getting `a • 0 = 0` (with `smul` coming from `smul_zero_class`). Apparently having both the type and instance differ is too hard for the unifier. Because we don't have definitional eta for structures yet, setting up the inheritance is a bit more tricky than you might think; I added an `example` test case to ensure everything stays OK. Co-authored-by: Mauricio Collares <mauricio@collares.org> Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>