mathlib3 documentation

ring_theory.integral_domain

Integral domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Assorted theorems about integral domains.

Main theorems #

TODO #

Prove Wedderburn's little theorem, which shows that all finite division rings are actually fields.

Tags #

integral domain, finite integral domain, finite field

theorem mul_right_bijective_of_finite₀ {M : Type u_1} [cancel_monoid_with_zero M] [finite M] {a : M} (ha : a 0) :
function.bijective (λ (b : M), a * b)
theorem mul_left_bijective_of_finite₀ {M : Type u_1} [cancel_monoid_with_zero M] [finite M] {a : M} (ha : a 0) :
function.bijective (λ (b : M), b * a)

Every finite nontrivial cancel_monoid_with_zero is a group_with_zero.

Equations
theorem exists_eq_pow_of_mul_eq_pow_of_coprime {R : Type u_1} [comm_semiring R] [is_domain R] [gcd_monoid R] [unique Rˣ] {a b c : R} {n : } (cp : is_coprime a b) (h : a * b = c ^ n) :
(d : R), a = d ^ n
theorem finset.exists_eq_pow_of_mul_eq_pow_of_coprime {ι : Type u_1} {R : Type u_2} [comm_semiring R] [is_domain R] [gcd_monoid R] [unique Rˣ] {n : } {c : R} {s : finset ι} {f : ι R} (h : (i : ι), i s (j : ι), j s i j is_coprime (f i) (f j)) (hprod : s.prod (λ (i : ι), f i) = c ^ n) (i : ι) (H : i s) :
(d : R), f i = d ^ n

Every finite domain is a division ring.

TODO: Prove Wedderburn's little theorem, which shows a finite domain is in fact commutative, hence a field.

Equations

Every finite commutative domain is a field.

TODO: Prove Wedderburn's little theorem, which shows a finite domain is automatically commutative, dropping one assumption from this theorem.

Equations
theorem card_nth_roots_subgroup_units {R : Type u_1} {G : Type u_2} [comm_ring R] [is_domain R] [group G] [fintype G] (f : G →* R) (hf : function.injective f) {n : } (hn : 0 < n) (g₀ : G) :
theorem is_cyclic_of_subgroup_is_domain {R : Type u_1} {G : Type u_2} [comm_ring R] [is_domain R] [group G] [finite G] (f : G →* R) (hf : function.injective f) :

A finite subgroup of the unit group of an integral domain is cyclic.

@[protected, instance]
def units.is_cyclic {R : Type u_1} [comm_ring R] [is_domain R] [finite Rˣ] :

The unit group of a finite integral domain is cyclic.

To support ℤˣ and other infinite monoids with finite groups of units, this requires only finite rather than deducing it from finite R.

@[protected, instance]

A finite subgroup of the units of an integral domain is cyclic.

theorem polynomial.div_eq_quo_add_rem_div {R : Type u_1} [comm_ring R] [is_domain R] (K : Type) [field K] [algebra (polynomial R) K] [is_fraction_ring (polynomial R) K] (f : polynomial R) {g : polynomial R} (hg : g.monic) :
(q r : polynomial R), r.degree < g.degree f / g = q + r / g
theorem card_fiber_eq_of_mem_range {G : Type u_2} [group G] [fintype G] {H : Type u_1} [group H] [decidable_eq H] (f : G →* H) {x y : H} (hx : x set.range f) (hy : y set.range f) :
(finset.filter (λ (g : G), f g = x) finset.univ).card = (finset.filter (λ (g : G), f g = y) finset.univ).card
theorem sum_hom_units_eq_zero {R : Type u_1} {G : Type u_2} [comm_ring R] [is_domain R] [group G] [fintype G] (f : G →* R) (hf : f 1) :
finset.univ.sum (λ (g : G), f g) = 0

In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero.

theorem sum_hom_units {R : Type u_1} {G : Type u_2} [comm_ring R] [is_domain R] [group G] [fintype G] (f : G →* R) [decidable (f = 1)] :
finset.univ.sum (λ (g : G), f g) = ite (f = 1) (fintype.card G) 0

In an integral domain, a sum indexed by a homomorphism from a finite group is zero, unless the homomorphism is trivial, in which case the sum is equal to the cardinality of the group.