Integral domains

Assorted theorems about 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} [CancelMonoidWithZero M] [Finite M] {a : M} (ha : a ≠ 0) : Function.Bijective fun (b : M) => a * b

theorem mul_left_bijective_of_finite₀ {M : Type u_1} [CancelMonoidWithZero M] [Finite M] {a : M} (ha : a ≠ 0) : Function.Bijective fun (b : M) => b * a

def Fintype.groupWithZeroOfCancel (M : Type u_2) [CancelMonoidWithZero M] [DecidableEq M] [Fintype M] [Nontrivial M] : GroupWithZero M

Every finite nontrivial cancel_monoid_with_zero is a group_with_zero.

Equations

• Fintype.groupWithZeroOfCancel M = let __src := inst; let __src_1 := inst✝²; GroupWithZero.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯

theorem exists_eq_pow_of_mul_eq_pow_of_coprime {R : Type u_2} [CommSemiring R] [IsDomain R] [GCDMonoid R] [Unique Rˣ] {a : R} {b : R} {c : R} {n : ℕ} (cp : IsCoprime a b) (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} [CommSemiring R] [IsDomain R] [GCDMonoid R] [Unique Rˣ] {n : ℕ} {c : R} {s : Finset ι} {f : ι → R} (h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (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] [IsDomain R] [DecidableEq R] [Fintype R] : DivisionRing 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.

def Fintype.fieldOfDomain (R : Type u_3) [CommRing R] [IsDomain R] [DecidableEq R] [Fintype R] : Field R

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

Equations

• Fintype.fieldOfDomain R = let __src := Fintype.divisionRingOfIsDomain R; let __src_1 := inst✝²; Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.qsmul ⋯

theorem Finite.isField_of_domain (R : Type u_3) [CommRing R] [IsDomain R] [Finite R] : IsField R

theorem card_nthRoots_subgroup_units {R : Type u_1} {G : Type u_2} [CommRing R] [IsDomain R] [Group G] [Fintype G] [DecidableEq G] (f : G →* R) (hf : Function.Injective ⇑f) {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} [CommRing R] [IsDomain R] [Group G] [Finite G] (f : G →* R) (hf : Function.Injective ⇑f) : IsCyclic G

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

instance instIsCyclicUnitsToMonoidToMonoidWithZeroToSemiringToCommSemiringInstGroup {R : Type u_1} [CommRing R] [IsDomain R] [Finite Rˣ] : IsCyclic 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 Finite Rˣ rather than deducing it from Finite R.

Equations

• ⋯ = ⋯

instance subgroup_units_cyclic {R : Type u_1} [CommRing R] [IsDomain R] (S : Subgroup Rˣ) [Finite ↥S] : IsCyclic ↥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} [CommRing R] [IsDomain R] (K : Type) [Field K] [Algebra (Polynomial R) K] [IsFractionRing (Polynomial R) K] (f : Polynomial R) {g : Polynomial R} (hg : Polynomial.Monic g) : ∃ (q : Polynomial R) (r : Polynomial R), Polynomial.degree r < Polynomial.degree g ∧ (algebraMap (Polynomial R) K) f / (algebraMap (Polynomial R) K) g = (algebraMap (Polynomial R) K) q + (algebraMap (Polynomial R) K) r / (algebraMap (Polynomial R) K) g

theorem card_fiber_eq_of_mem_range {G : Type u_2} [Group G] [Fintype G] {H : Type u_3} [Group H] [DecidableEq H] (f : G →* H) {x : H} {y : H} (hx : x ∈ Set.range ⇑f) (hy : y ∈ Set.range ⇑f) : (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} [CommRing R] [IsDomain R] [Group G] [Fintype G] (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} [CommRing R] [IsDomain R] [Group G] [Fintype G] (f : G →* R) [Decidable (f = 1)] : (Finset.sum Finset.univ fun (g : G) => f g) = ↑(if f = 1 then Fintype.card G 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.