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 = GroupWithZero.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯

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

• Fintype.divisionRingOfIsDomain R = DivisionRing.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯

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 = Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯ ⋯ 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 ≤ (Polynomial.nthRoots n (f g₀)).card

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 instIsCyclicUnitsOfFinite {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.

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.

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 : g.Monic) : ∃ (q : Polynomial R) (r : Polynomial R), r.degree < g.degree ∧ (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

@[deprecated MonoidHom.card_fiber_eq_of_mem_range (since := "2024-06-10")]

theorem card_fiber_eq_of_mem_range {G : Type u_1} {M : Type u_2} {F : Type u_3} [Group G] [Fintype G] [Monoid M] [DecidableEq M] [FunLike F G M] [MonoidHomClass F G M] (f : F) {x y : M} (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

Alias of MonoidHom.card_fiber_eq_of_mem_range.

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) : ∑ 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)] : ∑ 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.