Structures · Algebra
Valuation.RankLeOne
A valuation has rank at most one if its image (defined as MonoidWithZeroHom.valueGroup₀ v)
is contained in ℝ≥0. Note that this class includes the data
of an inclusion morphism MonoidWithZeroHom.valueGroup₀ v → ℝ≥0.
- Defined in
- Mathlib.RingTheory.Valuation.RankOne
- Shape
- One type argument · adds hom', strictMono'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by5
Ancestors0
No ancestors.