Conversion between multiplicative and additive definitions
add_submonoid.of_submonoid: convert between multiplicative and additive submonoids of
multiplicative M, and
submonoid.add_submonoid_equiv: equivalence between
add_submonoid (additive M).
(Commutative) monoid structure on a submonoid
submonoid.to_comm_monoid: a submonoid inherits a (commutative) monoid structure.
Operations on submonoids
submonoid.comap: preimage of a submonoid under a monoid homomorphism as a submonoid of the domain;
submonoid.map: image of a submonoid under a monoid homomorphism as a submonoid of the codomain;
submonoid.prod: product of two submonoids
s : submonoid Mand
t : submonoid Nas a submonoid of
M × N;
Monoid homomorphisms between submonoid
submonoid.subtype: embedding of a submonoid into the ambient monoid.
submonoid.inclusion: given two submonoids
S ≤ T,
S.inclusion Tis the inclusion of
Tas a monoid homomorphism;
mul_equiv.submonoid_congr: converts a proof of
S = Tinto a monoid isomorphism between
submonoid.prod_equiv: monoid isomorphism between
s × t;
monoid_hom.mrange: range of a monoid homomorphism as a submonoid of the codomain;
monoid_hom.mrestrict: restrict a monoid homomorphism to a submonoid;
monoid_hom.cod_mrestrict: restrict the codomain of a monoid homomorphism to a submonoid;
monoid_hom.mrange_restrict: restrict a monoid homomorphism to its range;
submonoid, range, product, map, comap
Submonoids of monoid
M are isomorphic to additive submonoids of
map f and
comap f form a
f is injective.
The product of submonoids is isomorphic to their product as monoids.
Restriction of a monoid hom to a submonoid of the codomain.
Makes the identity isomorphism from a proof that two submonoids of a multiplicative monoid are equal.