Rings with finite quotients

A commutative ring is said to have finite quotients if, for any nonzero ideal I of R, the quotient R ⧸ I is finite.

Main results

• Ring.HasFiniteQuotients.instDimensionLEOne: A ring with finite quotients has dimension ≤ 1.
• Ring.HasFiniteQuotients.instIsNoetherianRing : A ring with finite quotients is noetherian.
• Ring.HasFiniteQuotients.of_module_finite: Assume that R has finite quotients and that S is a domain and a finite R-module. Then S has finite quotients.
• Ring.HasFiniteQuotients.instOfIsDomainOfFiniteInt: A domain that is also a finite ℤ-module has finite quotients.

class Ring.HasFiniteQuotients (R : Type u_1) [CommRing R] : Prop

A ring R has finite quotients if the quotient R ⧸ I is finite for all nonzero ideals of R.

• finiteQuotient {I : Ideal R} : I ≠ ⊥ → Finite (R ⧸ I)

instance Ring.HasFiniteQuotients.instOfFinite {R : Type u_1} [CommRing R] [Finite R] : HasFiniteQuotients R

A finite ring has finite quotients.

theorem Ring.HasFiniteQuotients.maximalOfPrime {R : Type u_1} [CommRing R] [HasFiniteQuotients R] {P : Ideal R} [P.IsPrime] (hp : P ≠ ⊥) : P.IsMaximal

A nonzero prime ideal of a ring with finite quotients is maximal.

instance Ring.HasFiniteQuotients.instDimensionLEOne {R : Type u_1} [CommRing R] [HasFiniteQuotients R] : DimensionLEOne R

A ring with finite quotients has dimension ≤ 1.

instance Ring.HasFiniteQuotients.instIsNoetherianRing {R : Type u_1} [CommRing R] [HasFiniteQuotients R] : IsNoetherianRing R

A ring with finite quotients is noetherian.

theorem Ring.HasFiniteQuotients.of_module_finite (R : Type u_1) [CommRing R] [h : HasFiniteQuotients R] (S : Type u_2) [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S] : HasFiniteQuotients S

Assume that R has finite quotients and that S is a domain and a finite R-module. Then S has finite quotients.

instance Ring.HasFiniteQuotients.instInt : HasFiniteQuotients ℤ

The ring ℤ has finite quotients.

instance Ring.HasFiniteQuotients.instOfIsDomainOfFiniteInt {R : Type u_1} [CommRing R] [IsDomain R] [Module.Finite ℤ R] : HasFiniteQuotients R

A domain that is also a finite ℤ-module has finite quotients.