Unbundled monoid and group homomorphisms #
This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.
This file defines predicates for unbundled monoid and group homomorphisms. Instead of using
this file, please use
monoid_hom, defined in
algebra.hom.group, with notation
morphisms between monoids or groups. For example use
φ : G →* H to represent a group
homomorphism between multiplicative groups, and
ψ : A →+ B to represent a group homomorphism
between additive groups.
Main Definitions #
The composite of two additive monoid homomorphisms is an additive monoid homomorphism.
The composition of two additive group homomorphisms is an additive group homomorphism.
The sum of two additive group homomorphisms is an additive group homomorphism if the target is commutative.
These instances look redundant, because
is_ring_hom for a
Nevertheless these are harmless, and helpful for stripping out dependencies on
The difference of two additive group homomorphisms is an additive group homomorphism if the target is commutative.