Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-03 12:03 f6273d4d

View on Github →

feat(group_theory/group_action/sub_mul_action): Add an object for bundled sets closed under a mul action (#4996) This adds sub_mul_action as a base class for submodule, and copies across the relevant lemmas. This also weakens the type class requires for A →[R] B, to allow it to be used when only has_scalar is available.

Estimated changes

modified def mul_action_hom.comp
modified theorem mul_action_hom.comp_apply
modified theorem mul_action_hom.comp_id
modified theorem mul_action_hom.ext
modified theorem mul_action_hom.ext_iff
modified theorem mul_action_hom.id_apply
modified theorem mul_action_hom.id_comp
modified theorem mul_action_hom.map_smul
modified theorem submodule.neg_mem
added theorem sub_mul_action.coe_mem
added theorem sub_mul_action.coe_mk
added theorem sub_mul_action.coe_neg
added theorem sub_mul_action.ext
added theorem sub_mul_action.mem_coe
added theorem sub_mul_action.neg_mem
added structure sub_mul_action