Unbundled semiring and ring homomorphisms (deprecated)
This file defines typeclasses for unbundled semiring and ring homomorphisms. Though these classes are deprecated, they are still widely 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
is_semiring_hom (deprecated), is_ring_hom (deprecated)
Tags
is_semiring_hom, is_ring_hom
- map_zero : f 0 = 0
- map_one : f 1 = 1
- map_add : ∀ {x y : α}, f (x + y) = f x + f y
- map_mul : ∀ {x y : α}, f (x * y) = f x * f y
Predicate for semiring homomorphisms (deprecated -- use the bundled ring_hom version).
Instances
- is_ring_hom.is_semiring_hom
- is_semiring_hom.id
- ring_hom.is_semiring_hom
- polynomial.eval₂.is_semiring_hom
- polynomial.is_semiring_hom_C_f
- polynomial.map.is_semiring_hom
- polynomial.eval.is_semiring_hom
- mv_polynomial.eval₂.is_semiring_hom
- mv_polynomial.is_semiring_hom_sum_to_iter
- polynomial.is_semiring_hom
The identity map is a semiring homomorphism.
Equations
The composition of two semiring homomorphisms is a semiring homomorphism.
A semiring homomorphism is an additive monoid homomorphism.
Equations
- _ = _
A semiring homomorphism is a monoid homomorphism.
Equations
- _ = _
A map of rings that is a semiring homomorphism is also a ring homomorphism.
Ring homomorphisms map zero to zero.
Ring homomorphisms preserve additive inverses.
Ring homomorphisms preserve subtraction.
The identity map is a ring homomorphism.
Equations
The composition of two ring homomorphisms is a ring homomorphism.
A ring homomorphism is also a semiring homomorphism.
Equations
- _ = _
Equations
Interpret f : α → β with is_semiring_hom f as a ring homomorphism.
Equations
- _ = _
Equations
- _ = _