Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-01 07:42 67f3fdea

View on Github →

feat(algebra/group_ring_action) define group actions on rings (#2566) Define group action on rings. Related Zulip discussions:

Estimated changes

Created src/algebra/group_ring_action.lean

added def add_monoid.End

added def distrib_mul_action.hom_add_monoid_hom

added def distrib_mul_action.to_add_equiv

added def distrib_mul_action.to_add_monoid_hom

added def monoid.End

added def mul_semiring_action.to_semiring_equiv

added def mul_semiring_action.to_semiring_hom

added theorem smul_inv

added theorem smul_mul'

added theorem smul_pow

Modified src/group_theory/group_action.lean