Documentation

Mathlib.RingTheory.IntegralDomain

Integral domains #

Assorted theorems about integral domains.

Main theorems #

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

Every finite nontrivial cancel_monoid_with_zero is a group_with_zero.

Equations
Instances For
    theorem exists_eq_pow_of_mul_eq_pow_of_coprime {R : Type u_2} [CommSemiring R] [IsDomain R] [GCDMonoid R] [Subsingleton 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] [Subsingleton Rˣ] {n : } {c : R} {s : Finset ι} {f : ιR} (h : is, js, i jIsCoprime (f i) (f j)) (hprod : is, f i = c ^ n) (i : ι) :
    i s∃ (d : R), f i = d ^ n

    Every finite domain is a division ring. More generally, they are fields; this can be found in Mathlib.RingTheory.LittleWedderburn.

    Equations
    Instances For

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

      Equations
      Instances For
        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) :

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

        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 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] :

        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 : 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]
        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 : M} {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.