In analogy with the usual monoid action on a Type
M, we introduce an action of a
monoid_with_zero on a Type with
In particular, for Types
M, both containing
0, we define
smul_with_zero R M to
be the typeclass where the products
r • 0 and
0 • m vanish for all
r : R and all
m : M.
Moreover, in the case in which
R is a
monoid_with_zero, we introduce the typeclass
mul_action_with_zero R M, mimicking group actions and having an absorbing
Thus, the action is required to be compatible with
- the unit of the monoid, acting as the identity;
- the zero of the monoid_with_zero, acting as zero;
- associativity of the monoid.
We also add an
smul_with_zero is a class consisting of a Type
0 ∈ R and a scalar multiplication
R on a Type
0, such that the equality
r • m = 0 holds if at least one among
smul_with_zero structure along an injective zero-preserving homomorphism.
smul_with_zero structure along a surjective zero-preserving homomorphism.
An action of a monoid with zero
R on a Type
M, also with
is compatible with
0 (both in
R and in
1 ∈ R, and with associativity of
multiplication on the monoid
mul_action_with_zero structure along an injective zero-preserving homomorphism.
mul_action_with_zero structure along a surjective zero-preserving homomorphism.