Group action on rings #
This file defines the typeclass of monoid acting on semirings
MulSemiringAction 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
- smul : M → R → R
1by a scalar gives
Scalar multiplication distributes across multiplication
Typeclass for multiplicative actions by monoids on semirings.