Group action on rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines the typeclass of monoid acting on semirings
mul_semiring_action M R,
and the corresponding typeclass of invariant subrings.
algebra does not satisfy the axioms of
Implementation notes #
There is no separate typeclass for group acting on rings, group acting on fields, etc.
They are all grouped under
group action, invariant subring
Typeclass for multiplicative actions by monoids on semirings.
Instances of this typeclass
Instances of other typeclasses for
Each element of the monoid defines a semiring homomorphism.
Each element of the group defines a semiring isomorphism.
smul_inv' refers to the group case, and
smul_inv has an additional inverse