Unbundled semiring and ring homomorphisms (deprecated) #
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 semiring and ring homomorphisms. Instead of using
this file, please use RingHom
, defined in Algebra.Hom.Ring
, with notation →+*→+*
, for
morphisms between semirings or rings. For example use φ : A →+* B→+* B
to represent a
ring homomorphism.
Main Definitions #
IsSemiringHom
(deprecated), IsRingHom
(deprecated)
Tags #
IsSemiringHom, IsRingHom
The proposition that
f
preserves the additive identity.map_zero : f 0 = 0The proposition that
f
preserves the multiplicative identity.map_one : f 1 = 1The proposition that
f
preserves addition.The proposition that
f
preserves multiplication.
Predicate for semiring homomorphisms (deprecated -- use the bundled RingHom
version).
Instances For
The identity map is a semiring homomorphism.
The composition of two semiring homomorphisms is a semiring homomorphism.
A semiring homomorphism is an additive monoid homomorphism.
A semiring homomorphism is a monoid homomorphism.
A map of rings that is a semiring homomorphism is also a ring homomorphism.
Interpret f : α → β→ β
with IsSemiringHom f
as a ring homomorphism.
Equations
- One or more equations did not get rendered due to their size.