Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-17 09:57 54441b5d

View on Github →

feat(algebra/group_action_hom): define equivariant maps (#2866)

Estimated changes

Created src/algebra/group_action_hom.lean

added theorem distrib_mul_action_hom.coe_fn_coe'

added theorem distrib_mul_action_hom.coe_fn_coe

added def distrib_mul_action_hom.comp

added theorem distrib_mul_action_hom.comp_apply

added theorem distrib_mul_action_hom.comp_id

added theorem distrib_mul_action_hom.ext

added theorem distrib_mul_action_hom.ext_iff

added theorem distrib_mul_action_hom.id_apply

added theorem distrib_mul_action_hom.id_comp

added theorem distrib_mul_action_hom.map_add

added theorem distrib_mul_action_hom.map_neg

added theorem distrib_mul_action_hom.map_smul

added theorem distrib_mul_action_hom.map_sub

added theorem distrib_mul_action_hom.map_zero

added structure distrib_mul_action_hom

added def mul_action_hom.comp

added theorem mul_action_hom.comp_apply

added theorem mul_action_hom.comp_id

added theorem mul_action_hom.ext

added theorem mul_action_hom.ext_iff

added theorem mul_action_hom.id_apply

added theorem mul_action_hom.id_comp

added theorem mul_action_hom.map_smul

added def mul_action_hom.to_quotient

added theorem mul_action_hom.to_quotient_apply

added structure mul_action_hom

added theorem mul_semiring_action_hom.coe_fn_coe'

added theorem mul_semiring_action_hom.coe_fn_coe

added def mul_semiring_action_hom.comp

added theorem mul_semiring_action_hom.comp_apply

added theorem mul_semiring_action_hom.comp_id

added theorem mul_semiring_action_hom.ext

added theorem mul_semiring_action_hom.ext_iff

added theorem mul_semiring_action_hom.id_apply

added theorem mul_semiring_action_hom.id_comp

added theorem mul_semiring_action_hom.map_add

added theorem mul_semiring_action_hom.map_mul

added theorem mul_semiring_action_hom.map_neg

added theorem mul_semiring_action_hom.map_one

added theorem mul_semiring_action_hom.map_smul

added theorem mul_semiring_action_hom.map_sub

added theorem mul_semiring_action_hom.map_zero

added structure mul_semiring_action_hom