# 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.

## Notes #

Wedderburn's little theorem, which shows that all finite division rings are actually fields, is in Mathlib.RingTheory.LittleWedderburn.

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

Every finite nontrivial cancel_monoid_with_zero is a group_with_zero.

Equations
• = let __src := inst; let __src_1 := inst✝²; GroupWithZero.mk zpowRec
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 : R), 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 : is, js, i jIsCoprime (f i) (f j)) (hprod : (Finset.prod s fun (i : ι) => f i) = c ^ n) (i : ι) :
i s∃ (d : R), f i = d ^ n
def Fintype.divisionRingOfIsDomain (R : Type u_3) [Ring R] [] [] [] :

Every finite domain is a division ring. More generally, they are fields; this can be found in Mathlib.RingTheory.LittleWedderburn.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Fintype.fieldOfDomain (R : Type u_3) [] [] [] [] :

Every finite commutative domain is a field. More generally, commutativity is not required: this can be found in Mathlib.RingTheory.LittleWedderburn.

Equations
• = let __src := ; let __src_1 := inst✝²; Field.mk DivisionRing.zpow DivisionRing.qsmul
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.filter (fun (g : G) => g ^ n = g₀) Finset.univ).card 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.

Equations
• =
instance subgroup_units_cyclic {R : Type u_1} [] [] (S : ) [Finite S] :

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

Equations
• =
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.filter (fun (g : G) => f g = x) Finset.univ).card = (Finset.filter (fun (g : G) => f g = y) Finset.univ).card
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 : 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 : 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.