Structures · Algebra
ValuationRing
An integral domain is called a ValuationRing provided that for any pair
of elements a b : A, either a divides b or vice versa.
- Shape
- One type argument
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- ArchimedeanClass.FiniteElement
- AlgebraicGeometry.ValuativeCommSq.R
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- ValuationRing.mem_integer_iff
- ValuationRing.valuation
- ValuationRing.isInteger_or_isInteger
- bijective_rangeRestrict_comp_of_valuationRing
- WeierstrassCurve.exists_isIntegral
- ValuationRing.equivInteger
- AlgebraicGeometry.Proj.valuativeCriterion_existence_aux
- ValuationRing.coe_equivInteger_apply
- ValuationRing.instIsBezout
- ValuationRing.le_total
- ValuationRing.linearOrderedCommGroupWithZero
- ValuationRing.isFractionRing_iff
- ValuationRing.range_algebraMap_eq
- ValuationRing.toPreValuationRing
- ValuationRing.linearOrder