# mathlibdocumentation

ring_theory.integral_domain

# Integral domains #

## Main theorems #

• is_cyclic_of_subgroup_is_domain: A finite subgroup of the units of an integral domain is cyclic.
• fintype.field_of_domain: 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_fintype₀ {M : Type u_1} [fintype M] {a : M} (ha : a 0) :
function.bijective (λ (b : M), a * b)
theorem mul_left_bijective_of_fintype₀ {M : Type u_1} [fintype 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
def fintype.division_ring_of_is_domain (R : Type u_1) [ring R] [is_domain R] [decidable_eq R] [fintype 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.

Equations
def fintype.field_of_domain (R : Type u_1) [comm_ring R] [is_domain R] [decidable_eq R] [fintype R] :

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 fintype.is_field_of_domain (R : Type u_1) [comm_ring R] [is_domain R] [fintype R] :
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) :
{g ∈ finset.univ | g ^ n = g₀}.card multiset.card (f g₀))
theorem is_cyclic_of_subgroup_is_domain {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) :

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

@[protected, instance]
def subgroup_units_cyclic {R : Type u_1} [comm_ring R] [is_domain R] (S : subgroup Rˣ) [fintype S] :

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

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 ) (hy : y ) :
(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.