# Documentation

Mathlib.RingTheory.IntegralDomain

# Integral domains #

## Main theorems #

• isCyclic_of_subgroup_isDomain: A finite subgroup of the units of an integral domain is cyclic.
• Fintype.fieldOfDomain: A finite integral domain is a field.

## 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} [] {a : M} (ha : a 0) :
Function.Bijective fun b => a * b
theorem mul_left_bijective_of_finite₀ {M : Type u_1} [] {a : M} (ha : a 0) :
Function.Bijective fun b => b * a
def Fintype.groupWithZeroOfCancel (M : Type u_2) [] [] [] :

Every finite nontrivial cancel_monoid_with_zero is a group_with_zero.

Instances For
theorem exists_eq_pow_of_mul_eq_pow_of_coprime {R : Type u_2} [] [] [] [] {a : R} {b : R} {c : R} {n : } (cp : ) (h : a * b = c ^ n) :
d, a = d ^ n
theorem Finset.exists_eq_pow_of_mul_eq_pow_of_coprime {ι : Type u_2} {R : Type u_3} [] [] [] [] {n : } {c : R} {s : } {f : ιR} (h : ∀ (i : ι), i s∀ (j : ι), j si jIsCoprime (f i) (f j)) (hprod : (Finset.prod s fun i => f i) = c ^ n) (i : ι) :
i sd, f i = d ^ n
def Fintype.divisionRingOfIsDomain (R : Type u_3) [Ring R] [] [] [] :

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.

Instances For
def Fintype.fieldOfDomain (R : Type u_3) [] [] [] [] :

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.

Instances For
theorem Finite.isField_of_domain (R : Type u_3) [] [] [] :
theorem card_nthRoots_subgroup_units {R : Type u_1} {G : Type u_2} [] [] [] [] [] (f : G →* R) (hf : ) {n : } (hn : 0 < n) (g₀ : G) :
Finset.card (Finset.filter (fun g => g ^ n = g₀) Finset.univ) Multiset.card (Polynomial.nthRoots n (f g₀))
theorem isCyclic_of_subgroup_isDomain {R : Type u_1} {G : Type u_2} [] [] [] [] (f : G →* R) (hf : ) :

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

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 Rˣ rather than deducing it from Finite R.

instance subgroup_units_cyclic {R : Type u_1} [] [] (S : ) [Finite { x // x S }] :
IsCyclic { x // x S }

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

theorem Polynomial.div_eq_quo_add_rem_div {R : Type u_1} [] [] (K : Type) [] [Algebra () K] [] (f : ) {g : } (hg : ) :
q r, ↑(algebraMap () K) f / ↑(algebraMap () K) g = ↑(algebraMap () K) q + ↑(algebraMap () K) r / ↑(algebraMap () K) g
theorem card_fiber_eq_of_mem_range {G : Type u_2} [] [] {H : Type u_3} [] [] (f : G →* H) {x : H} {y : H} (hx : x ) (hy : y ) :
Finset.card (Finset.filter (fun g => f g = x) Finset.univ) = Finset.card (Finset.filter (fun g => f g = y) Finset.univ)
theorem sum_hom_units_eq_zero {R : Type u_1} {G : Type u_2} [] [] [] [] (f : G →* R) (hf : f 1) :
(Finset.sum Finset.univ fun 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} [] [] [] [] (f : G →* R) [Decidable (f = 1)] :
(Finset.sum Finset.univ fun g => f g) = ↑(if f = 1 then else 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.