This file proves simple properties of semirings, rings and domains and their unit groups. It also defines homomorphisms of semirings and rings, both unbundled (e.g. is_semiring_hom f) and bundled (e.g. ring_hom a β, a.k.a. α →+* β). The unbundled ones are deprecated and the plan is to slowly remove them from mathlib.
is_semiring_hom (deprecated), is_ring_hom (deprecated), ring_hom, nonzero_comm_semiring, nonzero_comm_ring, domain
→+* for bundled ring homs (also use for semiring homs)
There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.
There is no semiring_hom -- the idea is that ring_hom is used. The constructor for a ring_hom between semirings needs a proof of map_zero, map_one and map_add as well as map_mul; a separate constructor ring_hom.mk' will construct ring homs between rings from monoid homs given only a proof that addition is preserved.
Throughout the section on ring_hom implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type ring_hom. When they can be inferred from the type it is faster to use this method than to use type class inference.
is_ring_hom, is_semiring_hom, ring_hom, semiring_hom, semiring, comm_semiring, ring, comm_ring, domain, integral_domain, nonzero_comm_semiring, nonzero_comm_ring, units
Either zero and one are nonequal in a semiring, or the semiring is the zero ring.
If zero equals one in a semiring, the semiring is the zero ring.
If zero equals one in a semiring, all elements of that semiring are equal.
Each element of the group of units of a ring has an additive inverse.
Representing an element of a ring's unit group as an element of the ring commutes with mapping this element to its additive inverse.
Mapping an element of a ring's unit group to its inverse commutes with mapping this element to its additive inverse.
An element of a ring's unit group equals the additive inverse of its additive inverse.
Multiplication of elements of a ring's unit group commutes with mapping the first argument to its additive inverse.
Multiplication of elements of a ring's unit group commutes with mapping the second argument to its additive inverse.
Multiplication of the additive inverses of two elements of a ring's unit group equals multiplication of the two original elements.
The additive inverse of an element of a ring's unit group equals the additive inverse of one times the original element.
Predicate for semiring homomorphisms (deprecated -- use the bundled ring_hom version).
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.
An element of a ring multiplied by the additive inverse of one is the element's additive inverse.
The additive inverse of one multiplied by an element of a ring is the element's additive inverse.
An iff statement following from right distributivity in rings and the definition of subtraction.
A simplification of one side of an equation exploiting right distributivity in rings and the definition of subtraction.
If the product of two elements of a ring is nonzero, both elements are nonzero.
Given an element a of a commutative semiring, there exists another element whose product with zero equals a iff a equals zero.
Representation of a difference of two squares in a commutative ring as a product.
An element a of a commutative ring divides the additive inverse of an element b iff a divides b.
The additive inverse of an element a of a commutative ring divides another element b iff a divides b.
If an element a divides another element c in a commutative ring, a divides the sum of another element b with c iff a divides b.
If an element a divides another element b in a commutative ring, a divides the sum of b and another element c iff a divides c.
An element a divides the sum a + b if and only if a divides b.
An element a divides the sum b + a if and only if a divides b.
Vieta's formula for a quadratic equation, relating the coefficients of the polynomial with its roots. This particular version states that if we have a root x of a monic quadratic polynomial, then there is another root y such that x + y is negative the a_1 coefficient and x * y is the a_0 coefficient.
Predicate for ring homomorphisms (deprecated -- use the bundled ring_hom version).
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.
The composition of two ring homomorphisms is a ring homomorphism.
A ring homomorphism is also a semiring homomorphism.
Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.
Interpret f : α → β with is_semiring_hom f as a ring homomorphism.
Ring homomorphisms map zero to zero.
Ring homomorphisms map one to one.
Ring homomorphisms preserve addition.
Ring homomorphisms preserve multiplication.
The identity ring homomorphism from a semiring to itself.
Composition of ring homomorphisms is a ring homomorphism.
Ring homomorphisms preserve additive inverse.
Ring homomorphisms preserve subtraction.
Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition.
Predicate for commutative semirings in which zero does not equal one.
Predicate for commutative rings in which zero does not equal one.
A nonzero commutative ring is a nonzero commutative semiring.
An integral domain is a nonzero commutative ring.
An element of the unit group of a nonzero commutative semiring represented as an element of the semiring is nonzero.
Makes a nonzero commutative ring from a commutative ring containing at least two distinct elements.
Makes a nonzero commutative semiring from a commutative semiring containing at least two distinct elements.
this is needed for compatibility between Lean 3.4.2 and Lean 3.5.0c
A domain is a ring with no zero divisors, i.e. satisfying the condition a * b = 0 ↔ a = 0 ∨ b = 0. Alternatively, a domain is an integral domain without assuming commutativity of multiplication.
Simplification theorems for the definition of a domain.
The product of two nonzero elements of a domain is nonzero.
Right multiplication by a nonzero element in a domain is injective.
Left multiplication by a nonzero element in a domain is injective.
An element of a domain fixed by right multiplication by an element other than one must be zero.
An element of a domain fixed by left multiplication by an element other than one must be zero.
For elements a, b of a domain, if ab is nonzero, so is ba.
An integral domain is a domain.
Right multiplcation by a nonzero element of an integral domain is injective.
Left multiplication by a nonzero element of an integral domain is injective.
Given two elements b, c of an integral domain and a nonzero element a, ab divides ac iff b divides c.
Given two elements a, b of an integral domain and a nonzero element c, ac divides bc iff a divides b.
In the unit group of an integral domain, a unit is its own inverse iff the unit is one or one's additive inverse.
Elements of the unit group of a commutative semiring represented as elements of the semiring divide any element of the semiring.
In a commutative semiring, an element a divides an element b iff a divides all associates of b.
An element of a commutative semiring divides a unit iff the element divides one.
In a commutative semiring, an element a divides an element b iff all associates of a divide b.
Every unit in a domain is nonzero.