Properties and homomorphisms of semirings and rings
This file proves simple properties of semirings, rings and domains and their unit groups. It also
defines bundled homomorphisms of semirings and rings. As with monoid and groups, we use the same
structure ring_hom a β
, a.k.a. α →+* β
, for both homomorphism types.
The unbundled homomorphisms are defined in deprecated/ring
. They are deprecated and the plan is to
slowly remove them from mathlib.
Main definitions
ring_hom, nonzero, domain, integral_domain
Notations
→+* for bundled ring homs (also use for semiring homs)
Implementation notes
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.
Tags
ring_hom
, semiring_hom
, semiring
, comm_semiring
, ring
, comm_ring
, domain
,
integral_domain
, nonzero
, units
distrib
class
Pullback a distrib
instance along an injective function.
Equations
- function.injective.distrib f hf add mul = {mul := has_mul.mul _inst_1, add := has_add.add _inst_2, left_distrib := _, right_distrib := _}
Pushforward a distrib
instance along a surjective function.
Equations
- function.surjective.distrib f hf add mul = {mul := has_mul.mul _inst_3, add := has_add.add _inst_2, left_distrib := _, right_distrib := _}
Semirings
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
A semiring is a type with the following structures: additive commutative monoid
(add_comm_monoid
), multiplicative monoid (monoid
), distributive laws (distrib
), and
multiplication by zero law (mul_zero_class
). The actual definition extends monoid_with_zero
instead of monoid
and mul_zero_class
.
Instances
- comm_semiring.to_semiring
- ordered_semiring.to_semiring
- ring.to_semiring
- with_zero.semiring
- nat.semiring
- opposite.semiring
- int.semiring
- rat.semiring
- set.set_semiring.semiring
- pi.semiring
- matrix.semiring
- linear_map.endomorphism_semiring
- prod.semiring
- subsemiring.to_semiring
- algebra.comap.semiring
- submodule.semiring
- subalgebra.semiring
- monoid_algebra.semiring
- add_monoid_algebra.semiring
- free_algebra.semiring
- SemiRing.semiring
- polynomial.semiring
- SemiRing.semiring_obj
- SemiRing.limit_semiring
- Algebra.semiring_obj
- ring_quot.semiring
- tensor_algebra.semiring
- ulift.semiring
- continuous_map_semiring
- real.semiring
- mv_power_series.semiring
- power_series.semiring
- filter.germ.semiring
- language.semiring
- zsqrtd.semiring
- smooth_map_semiring
- algebra.tensor_product.tensor_product.semiring
- exterior_algebra.semiring
- nat.arithmetic_function.semiring
Pullback a semiring
instance along an injective function.
Equations
- function.injective.semiring f hf zero one add mul = {add := add_comm_monoid.add (function.injective.add_comm_monoid f hf zero add), add_assoc := _, zero := monoid_with_zero.zero (function.injective.monoid_with_zero f hf zero one mul), zero_add := _, add_zero := _, add_comm := _, mul := monoid_with_zero.mul (function.injective.monoid_with_zero f hf zero one mul), mul_assoc := _, one := monoid_with_zero.one (function.injective.monoid_with_zero f hf zero one mul), one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
Pullback a semiring
instance along an injective function.
Equations
- function.surjective.semiring f hf zero one add mul = {add := add_comm_monoid.add (function.surjective.add_comm_monoid f hf zero add), add_assoc := _, zero := monoid_with_zero.zero (function.surjective.monoid_with_zero f hf zero one mul), zero_add := _, add_zero := _, add_comm := _, mul := monoid_with_zero.mul (function.surjective.monoid_with_zero f hf zero one mul), mul_assoc := _, one := monoid_with_zero.one (function.surjective.monoid_with_zero f hf zero one mul), one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
Left multiplication by an element of a (semi)ring is an add_monoid_hom
Equations
- add_monoid_hom.mul_left r = {to_fun := has_mul.mul r, map_zero' := _, map_add' := _}
Right multiplication by an element of a (semi)ring is an add_monoid_hom
- to_fun : α → β
- map_one' : c.to_fun 1 = 1
- map_mul' : ∀ (x y : α), c.to_fun (x * y) = (c.to_fun x) * c.to_fun y
- map_zero' : c.to_fun 0 = 0
- map_add' : ∀ (x y : α), c.to_fun (x + y) = c.to_fun x + c.to_fun y
Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.
This extends from both monoid_hom
and monoid_with_zero_hom
in order to put the fields in a
sensible order, even though monoid_with_zero_hom
already extends monoid_hom
.
Reinterpret a ring homomorphism f : R →+* S
as a monoid_with_zero_hom R S
.
The simp
-normal form is (f : monoid_with_zero_hom R S)
.
Throughout this section, some semiring
arguments are specified with {}
instead of []
.
See note [implicit instance arguments].
Equations
- ring_hom.has_coe_to_fun = {F := λ (x : α →+* β), α → β, coe := ring_hom.to_fun rβ}
Equations
Equations
f : R →+* S
doesn't map 1
to 0
if S
is nontrivial
If there is a homomorphism f : R →+* S
and S
is nontrivial, then R
is nontrivial.
Equations
- ring_hom.inhabited = {default := ring_hom.id α rα}
Equations
- ring_hom.monoid = {mul := ring_hom.comp rα, mul_assoc := _, one := ring_hom.id α rα, one_mul := _, mul_one := _}
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- mul_comm : ∀ (a b : α), a * b = b * a
A commutative semiring is a semiring
with commutative multiplication. In other words, it is a
type with the following structures: additive commutative monoid (add_comm_monoid
), multiplicative
commutative monoid (comm_monoid
), distributive laws (distrib
), and multiplication by zero law
(mul_zero_class
).
Instances
- comm_ring.to_comm_semiring
- ordered_comm_semiring.to_comm_semiring
- canonically_ordered_comm_semiring.to_comm_semiring
- nat.comm_semiring
- int.comm_semiring
- rat.comm_semiring
- set.set_semiring.comm_semiring
- pi.comm_semiring
- prod.comm_semiring
- subsemiring.to_comm_semiring
- algebra.comap.comm_semiring
- submodule.comm_semiring
- subalgebra.comm_semiring
- monoid_algebra.comm_semiring
- add_monoid_algebra.comm_semiring
- CommSemiRing.comm_semiring
- polynomial.comm_semiring
- mv_polynomial.comm_semiring
- ideal.comm_semiring
- CommSemiRing.comm_semiring_obj
- CommSemiRing.limit_comm_semiring
- ring_quot.comm_semiring
- cardinal.comm_semiring
- triv_sq_zero_ext.comm_semiring
- ulift.comm_semiring
- real.comm_semiring
- nnreal.comm_semiring
- mv_power_series.comm_semiring
- power_series.comm_semiring
- filter.germ.comm_semiring
- num.comm_semiring
- zsqrtd.comm_semiring
- nat.arithmetic_function.comm_semiring
- ring.fractional_ideal.comm_semiring
Equations
- comm_semiring.to_comm_monoid_with_zero = {mul := comm_monoid.mul (comm_semiring.to_comm_monoid α), mul_assoc := _, one := comm_monoid.one (comm_semiring.to_comm_monoid α), one_mul := _, mul_one := _, mul_comm := _, zero := semiring.zero (comm_semiring.to_semiring α), zero_mul := _, mul_zero := _}
Pullback a semiring
instance along an injective function.
Equations
- function.injective.comm_semiring f hf zero one add mul = {add := semiring.add (function.injective.semiring f hf zero one add mul), add_assoc := _, zero := semiring.zero (function.injective.semiring f hf zero one add mul), zero_add := _, add_zero := _, add_comm := _, mul := semiring.mul (function.injective.semiring f hf zero one add mul), mul_assoc := _, one := semiring.one (function.injective.semiring f hf zero one add mul), one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
Pullback a semiring
instance along an injective function.
Equations
- function.surjective.comm_semiring f hf zero one add mul = {add := semiring.add (function.surjective.semiring f hf zero one add mul), add_assoc := _, zero := semiring.zero (function.surjective.semiring f hf zero one add mul), zero_add := _, add_zero := _, add_comm := _, mul := semiring.mul (function.surjective.semiring f hf zero one add mul), mul_assoc := _, one := semiring.one (function.surjective.semiring f hf zero one add mul), one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
Rings
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
A ring is a type with the following structures: additive commutative group (add_comm_group
),
multiplicative monoid (monoid
), and distributive laws (distrib
). Equivalently, a ring is a
semiring
with a negation operation making it an additive group.
Instances
- comm_ring.to_ring
- domain.to_ring
- ordered_ring.to_ring
- nonneg_ring.to_ring
- division_ring.to_ring
- normed_ring.to_ring
- opposite.ring
- int.ring
- pi.ring
- matrix.ring
- linear_map.endomorphism_ring
- prod.ring
- subring.to_ring
- algebra.comap.ring
- subalgebra.ring
- monoid_algebra.ring
- add_monoid_algebra.ring
- free_algebra.ring
- Ring.ring
- Algebra.is_ring
- polynomial.ring
- free_abelian_group.ring
- free_ring.ring
- ring.direct_limit.ring
- Ring.ring_obj
- Ring.limit_ring
- Algebra.limit_semiring
- ring_quot.ring
- tensor_algebra.ring
- universal_enveloping_algebra.ring
- ulift.ring
- continuous_linear_map.ring
- continuous_ring
- continuous_map_ring
- cau_seq.ring
- real.ring
- bounded_continuous_function.ring
- mv_power_series.ring
- power_series.ring
- filter.germ.ring
- quaternion_algebra.ring
- quaternion.ring
- Module.Mon_Module_equivalence_Algebra.Mon_.X.ring
- padic_int.ring
- zsqrtd.ring
- smooth_map_ring
- algebra.tensor_product.tensor_product.ring
- exterior_algebra.ring
- clifford_algebra.ring
- lucas_lehmer.X.ring
- perfection.ring
- uniform_space.completion.ring
Equations
Pullback a ring
instance along an injective function.
Equations
- function.injective.ring f hf zero one add mul neg = {add := add_comm_group.add (function.injective.add_comm_group f hf zero add neg), add_assoc := _, zero := add_comm_group.zero (function.injective.add_comm_group f hf zero add neg), zero_add := _, add_zero := _, neg := add_comm_group.neg (function.injective.add_comm_group f hf zero add neg), sub := add_comm_group.sub (function.injective.add_comm_group f hf zero add neg), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := monoid.mul (function.injective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
Pullback a ring
instance along an injective function,
with a subtraction (-
) that is not necessarily defeq to a + -b
.
Equations
- function.injective.ring_sub f hf zero one add mul neg sub = {add := add_comm_group.add (function.injective.add_comm_group_sub f hf zero add neg sub), add_assoc := _, zero := add_comm_group.zero (function.injective.add_comm_group_sub f hf zero add neg sub), zero_add := _, add_zero := _, neg := add_comm_group.neg (function.injective.add_comm_group_sub f hf zero add neg sub), sub := add_comm_group.sub (function.injective.add_comm_group_sub f hf zero add neg sub), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := monoid.mul (function.injective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
Pullback a ring
instance along an injective function.
Equations
- function.surjective.ring f hf zero one add mul neg = {add := add_comm_group.add (function.surjective.add_comm_group f hf zero add neg), add_assoc := _, zero := add_comm_group.zero (function.surjective.add_comm_group f hf zero add neg), zero_add := _, add_zero := _, neg := add_comm_group.neg (function.surjective.add_comm_group f hf zero add neg), sub := add_comm_group.sub (function.surjective.add_comm_group f hf zero add neg), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := monoid.mul (function.surjective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
Pullback a ring
instance along an injective function,
with a subtraction (-
) that is not necessarily defeq to a + -b
.
Equations
- function.surjective.ring_sub f hf zero one add mul neg sub = {add := add_comm_group.add (function.surjective.add_comm_group_sub f hf zero add neg sub), add_assoc := _, zero := add_comm_group.zero (function.surjective.add_comm_group_sub f hf zero add neg sub), zero_add := _, add_zero := _, neg := add_comm_group.neg (function.surjective.add_comm_group_sub f hf zero add neg sub), sub := add_comm_group.sub (function.surjective.add_comm_group_sub f hf zero add neg sub), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := monoid.mul (function.surjective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- mul_comm : ∀ (a b : α), a * b = b * a
A commutative ring is a ring
with commutative multiplication.
Instances
- integral_domain.to_comm_ring
- ordered_comm_ring.to_comm_ring
- field.to_comm_ring
- euclidean_domain.to_comm_ring
- normed_comm_ring.to_comm_ring
- opposite.comm_ring
- int.comm_ring
- rat.comm_ring
- pi.comm_ring
- prod.comm_ring
- subring.to_comm_ring
- algebra.comap.comm_ring
- subalgebra.comm_ring
- monoid_algebra.comm_ring
- add_monoid_algebra.comm_ring
- ideal.quotient.comm_ring
- punit.comm_ring
- CommRing.comm_ring
- polynomial.comm_ring
- mv_polynomial.comm_ring
- free_abelian_group.comm_ring
- free_comm_ring.comm_ring
- free_ring.comm_ring
- ring.direct_limit.comm_ring
- CommRing.comm_ring_obj
- CommRing.limit_comm_ring
- CommRing.colimits.colimit_type.comm_ring
- Module.category_theory.monoidal_category.tensor_unit.comm_ring
- ring_quot.comm_ring
- ulift.comm_ring
- zmod.comm_ring
- TopCommRing.is_comm_ring
- TopCommRing.forget_comm_ring
- TopCommRing.forget_to_Top_comm_ring
- continuous_comm_ring
- continuous_map_comm_ring
- localization_map.codomain.comm_ring
- localization.comm_ring
- algebraic_geometry.structure_sheaf.localizations.comm_ring
- algebraic_geometry.comm_ring_structure_sheaf_in_Type_obj
- cau_seq.comm_ring
- cau_seq.completion.Cauchy.comm_ring
- real.comm_ring
- complex.comm_ring
- bounded_continuous_function.comm_ring
- mv_power_series.comm_ring
- power_series.comm_ring
- adjoin_root.comm_ring
- filter.germ.comm_ring
- padic.comm_ring
- zsqrtd.comm_ring
- gaussian_int.comm_ring
- perfect_closure.comm_ring
- smooth_map_comm_ring
- algebra.tensor_product.tensor_product.comm_ring
- nat.arithmetic_function.comm_ring
- poly.comm_ring
- lucas_lehmer.X.comm_ring
- perfection.comm_ring
- mod_p.comm_ring
- pre_tilt.comm_ring
- witt_vector.comm_ring
- truncated_witt_vector.comm_ring
- uniform_space.completion.comm_ring
- uniform_space.comm_ring
- compare_reals.Q.comm_ring
Equations
- comm_ring.to_comm_semiring = {add := comm_ring.add s, add_assoc := _, zero := comm_ring.zero s, zero_add := _, add_zero := _, add_comm := _, mul := comm_ring.mul s, mul_assoc := _, one := comm_ring.one s, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
Pullback a comm_ring
instance along an injective function.
Equations
- function.injective.comm_ring f hf zero one add mul neg = {add := ring.add (function.injective.ring f hf zero one add mul neg), add_assoc := _, zero := ring.zero (function.injective.ring f hf zero one add mul neg), zero_add := _, add_zero := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg), sub := ring.sub (function.injective.ring f hf zero one add mul neg), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul (function.injective.ring f hf zero one add mul neg), mul_assoc := _, one := ring.one (function.injective.ring f hf zero one add mul neg), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
Pullback a comm_ring
instance along an injective function,
with a subtraction (-
) that is not necessarily defeq to a + -b
.
Equations
- function.injective.comm_ring_sub f hf zero one add mul neg sub = {add := ring.add (function.injective.ring_sub f hf zero one add mul neg sub), add_assoc := _, zero := ring.zero (function.injective.ring_sub f hf zero one add mul neg sub), zero_add := _, add_zero := _, neg := ring.neg (function.injective.ring_sub f hf zero one add mul neg sub), sub := ring.sub (function.injective.ring_sub f hf zero one add mul neg sub), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul (function.injective.ring_sub f hf zero one add mul neg sub), mul_assoc := _, one := ring.one (function.injective.ring_sub f hf zero one add mul neg sub), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
Pullback a comm_ring
instance along an injective function.
Equations
- function.surjective.comm_ring f hf zero one add mul neg = {add := ring.add (function.surjective.ring f hf zero one add mul neg), add_assoc := _, zero := ring.zero (function.surjective.ring f hf zero one add mul neg), zero_add := _, add_zero := _, neg := ring.neg (function.surjective.ring f hf zero one add mul neg), sub := ring.sub (function.surjective.ring f hf zero one add mul neg), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul (function.surjective.ring f hf zero one add mul neg), mul_assoc := _, one := ring.one (function.surjective.ring f hf zero one add mul neg), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
Pullback a comm_ring
instance along an injective function,
with a subtraction (-
) that is not necessarily defeq to a + -b
.
Equations
- function.surjective.comm_ring_sub f hf zero one add mul neg sub = {add := ring.add (function.surjective.ring_sub f hf zero one add mul neg sub), add_assoc := _, zero := ring.zero (function.surjective.ring_sub f hf zero one add mul neg sub), zero_add := _, add_zero := _, neg := ring.neg (function.surjective.ring_sub f hf zero one add mul neg sub), sub := ring.sub (function.surjective.ring_sub f hf zero one add mul neg sub), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul (function.surjective.ring_sub f hf zero one add mul neg sub), mul_assoc := _, one := ring.one (function.surjective.ring_sub f hf zero one add mul neg sub), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
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.
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- exists_pair_ne : ∃ (x y : α), x ≠ y
- eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0 → a = 0 ∨ b = 0
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.
Equations
- domain.to_cancel_monoid_with_zero = {mul := semiring.mul infer_instance, mul_assoc := _, one := semiring.one infer_instance, one_mul := _, mul_one := _, zero := semiring.zero infer_instance, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}
Pullback a domain
instance along an injective function.
Equations
- function.injective.domain f hf zero one add mul neg = {add := ring.add (function.injective.ring f hf zero one add mul neg), add_assoc := _, zero := ring.zero (function.injective.ring f hf zero one add mul neg), zero_add := _, add_zero := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg), sub := ring.sub (function.injective.ring f hf zero one add mul neg), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul (function.injective.ring f hf zero one add mul neg), mul_assoc := _, one := ring.one (function.injective.ring f hf zero one add mul neg), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
Integral domains
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- mul_comm : ∀ (a b : α), a * b = b * a
- exists_pair_ne : ∃ (x y : α), x ≠ y
- eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0 → a = 0 ∨ b = 0
An integral domain is a commutative ring with no zero divisors, i.e. satisfying the condition
a * b = 0 ↔ a = 0 ∨ b = 0
. Alternatively, an integral domain is a domain with commutative
multiplication.
Instances
- euclidean_domain.integral_domain
- linear_ordered_comm_ring.to_integral_domain
- field.to_integral_domain
- opposite.integral_domain
- rat.integral_domain
- subring.subring.domain
- subalgebra.integral_domain
- ideal.quotient.integral_domain
- polynomial.integral_domain
- mv_polynomial.integral_domain
- integral_closure.integral_domain
- localization_map.integral_domain_of_local_at_prime
- real.integral_domain
- power_series.integral_domain
- padic_int.integral_domain
- zsqrtd.integral_domain
- pre_tilt.integral_domain
Equations
- integral_domain.to_comm_cancel_monoid_with_zero = {mul := comm_monoid_with_zero.mul comm_semiring.to_comm_monoid_with_zero, mul_assoc := _, one := comm_monoid_with_zero.one comm_semiring.to_comm_monoid_with_zero, one_mul := _, mul_one := _, mul_comm := _, zero := comm_monoid_with_zero.zero comm_semiring.to_comm_monoid_with_zero, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}
Pullback an integral_domain
instance along an injective function.
Equations
- function.injective.integral_domain f hf zero one add mul neg = {add := comm_ring.add (function.injective.comm_ring f hf zero one add mul neg), add_assoc := _, zero := comm_ring.zero (function.injective.comm_ring f hf zero one add mul neg), zero_add := _, add_zero := _, neg := comm_ring.neg (function.injective.comm_ring f hf zero one add mul neg), sub := comm_ring.sub (function.injective.comm_ring f hf zero one add mul neg), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul (function.injective.comm_ring f hf zero one add mul neg), mul_assoc := _, one := comm_ring.one (function.injective.comm_ring f hf zero one add mul neg), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
In the unit group of an integral domain, a unit is its own inverse iff the unit is one or one's additive inverse.
Introduce a function inverse
on a ring R
, which sends x
to x⁻¹
if x
is invertible and
to 0
otherwise. This definition is somewhat ad hoc, but one needs a fully (rather than partially)
defined inverse function for some purposes, including for calculus.
Equations
- ring.inverse = λ (x : R), dite (is_unit x) (λ (h : is_unit x), ↑(classical.some h)⁻¹) (λ (h : ¬is_unit x), 0)
By definition, if x
is invertible then inverse x = x⁻¹
.
By definition, if x
is not invertible then inverse x = 0
.
- exists_pair_ne : ∃ (x y : R), x ≠ y
- mul_comm : ∀ (x y : R), x * y = y * x
- eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (x y : R), x * y = 0 → x = 0 ∨ y = 0
A predicate to express that a ring is an integral domain.
This is mainly useful because such a predicate does not contain data, and can therefore be easily transported along ring isomorphisms.
Every integral domain satisfies the predicate for integral domains.
If a ring satisfies the predicate for integral domains,
then it can be endowed with an integral_domain
instance
whose data is definitionally equal to the existing data.
Equations
- is_integral_domain.to_integral_domain R h = {add := ring.add _inst_1, add_assoc := _, zero := ring.zero _inst_1, zero_add := _, add_zero := _, neg := ring.neg _inst_1, sub := ring.sub _inst_1, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul _inst_1, mul_assoc := _, one := ring.one _inst_1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}