Commit 2022-09-23 14:45 8f66240c

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.