Elementwise monoid structure of additive submonoids #
These definitions are a cut-down versions of the ones around Submodule.mul
, as that API is
usually more useful.
SMul (AddSubmonoid R) (AddSubmonoid A)
is also provided given DistribSMul R A
,
and when R = A
it is definitionally equal to the multiplication on AddSubmonoid R
.
These are all available in the Pointwise
locale.
Additionally, it provides various degrees of monoid structure:
AddSubmonoid.one
AddSubmonoid.mul
AddSubmonoid.mulOneClass
AddSubmonoid.semigroup
AddSubmonoid.monoid
which is available globally to match the monoid structure implied by Submodule.idemSemiring
.
Implementation notes #
Many results about multiplication are derived from the corresponding results about scalar
multiplication, but results requiring right distributivity do not have SMul versions,
due to the lack of a suitable typeclass (unless one goes all the way to Module
).
If R
is an additive monoid with one (e.g., a semiring), then 1 : AddSubmonoid R
is the range
of Nat.cast : ℕ → R
.
Equations
Instances For
For M : Submonoid R
and N : AddSubmonoid A
, M • N
is the additive submonoid
generated by all m • n
where m ∈ M
and n ∈ N
.
Equations
Instances For
Multiplication of additive submonoids of a semiring R. The additive submonoid S * T
is the
smallest R-submodule of R
containing the elements s * t
for s ∈ S
and t ∈ T
.
Equations
Instances For
AddSubmonoid.neg
distributes over multiplication.
This is available as an instance in the Pointwise
locale.
Equations
Instances For
A MulOneClass
structure on additive submonoids of a (possibly, non-associative) semiring.
Equations
Instances For
Semigroup structure on additive submonoids of a (possibly, non-unital) semiring.
Equations
Instances For
Monoid structure on additive submonoids of a semiring.