Integral domains
Assorted theorems about integral domains.
Main theorems
is_cyclic_of_subgroup_integral_domain: A finite subgroup of the units of an integral domain is cyclic.field_of_integral_domain: A finite integral domain is a field.
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) :
function.injective ⇑f → is_cyclic G
A finite subgroup of the unit group of an integral domain is cyclic.
@[instance]
The unit group of a finite integral domain is cyclic.
Equations
def
field_of_integral_domain
{R : Type u_1}
[integral_domain R]
[decidable_eq R]
[fintype R] :
field R
Every finite integral domain is a field.
Equations
- field_of_integral_domain = {add := integral_domain.add (show integral_domain R, from _inst_1), add_assoc := _, zero := integral_domain.zero (show integral_domain R, from _inst_1), zero_add := _, add_zero := _, neg := integral_domain.neg (show integral_domain R, from _inst_1), add_left_neg := _, add_comm := _, mul := integral_domain.mul (show integral_domain R, from _inst_1), mul_assoc := _, one := integral_domain.one (show integral_domain R, from _inst_1), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := λ (a : R), dite (a = 0) (λ (h : a = 0), 0) (λ (h : ¬a = 0), fintype.bij_inv _ 1), exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
@[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.
Equations
- _ = _
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 ⇑f → 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}
[integral_domain R]
[group G]
[fintype G]
(f : G →* R) :
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}
[integral_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.