Structures · Algebra
Ring.HasFiniteQuotients
A ring R has finite quotients if the quotient R ⧸ I is finite for all nonzero ideals of R.
- Shape
- One type argument · adds finiteQuotient
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Int
How is a type an instance?
Loading the hierarchy index…
Assumed by24
- Ring.HasFiniteQuotients.finiteQuotient
- Ring.HasFiniteQuotients.finite_setOfPred_mem
- Ring.HasFiniteQuotients.finite_cardQuot_le
- IsInertiaField.rank_right
- Ring.HasFiniteQuotients.finite_cardQuot_heightOneSpectrum_le
- IsDecompositionField.ramificationIdxIn_eq
- IsInertiaField.rank_left
- IsDecompositionField.rank_left
- IsDecompositionField.rank_right
- IsDecompositionField.inertiaDegIn_eq
- Ring.HasFiniteQuotients.instNorthcottHeightOneSpectrumNatCoeMonoidWithZeroHomIdealAbsNormAsIdeal
- Ring.HasFiniteQuotients.finite_absNorm_le
- Ring.HasFiniteQuotients.finite_setOf_mem
- Ring.HasFiniteQuotients.instIsNoetherianRing
- IsDecompositionField.ramificationIdx_eq
- Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le
- IsInertiaField.rank_decompositionField
- IsDecompositionField.inertiaDeg_eq
- Ring.HasFiniteQuotients.instNorthcottIdealNatCardQuot
- Ring.HasFiniteQuotients.maximalOfPrime
- Ring.HasFiniteQuotients.instPerfectFieldResidueFieldOfFractionRing
- Ring.HasFiniteQuotients.cardQuot_pos
- Ring.HasFiniteQuotients.of_module_finite
- Ring.HasFiniteQuotients.instDimensionLEOne
Ancestors0
No ancestors.