mathlib documentation

ring_theory.integral_domain

Integral domains

Assorted theorems about integral domains.

Main theorems

Tags

integral domain, finite integral domain, finite field

theorem card_nth_roots_subgroup_units {R : Type u_1} {G : Type u_2} [integral_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 (polynomial.nth_roots n (f g₀)).card

theorem is_cyclic_of_subgroup_integral_domain {R : Type u_1} {G : Type u_2} [integral_domain R] [group G] [fintype G] (f : G →* R) :

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

@[instance]
def units.is_cyclic {R : Type u_1} [integral_domain R] [fintype R] :

The unit group of a finite integral domain is cyclic.

def field_of_integral_domain {R : Type u_1} [integral_domain R] [decidable_eq R] [fintype R] :

Every finite integral domain is a field.

Equations
@[instance]
def subgroup_units_cyclic {R : Type u_1} [integral_domain R] (S : set (units R)) [is_subgroup S] [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} :
x set.range fy 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} [integral_domain R] [group G] [fintype G] (f : G →* R) :
f 1∑ (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} [integral_domain R] [group G] [fintype G] (f : G →* R) [decidable (f = 1)] :
∑ (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.