Unbundled monoid and group homomorphisms #
This file defines predicates for unbundled monoid and group homomorphisms. Though bundled morphisms are preferred in mathlib, these unbundled predicates are still occasionally used in mathlib, and probably will not go away before Lean 4 because Lean 3 often fails to coerce a bundled homomorphism to a function.
Main Definitions #
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.