Structures · Algebra
ValuativeRel.IsNontrivial
We say that a valuative relation on a ring is nontrivial if the value group-with-zero is nontrivial, meaning that it has an element which is different from 0 and 1.
- Shape
- One type argument · adds condition
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- Padic
How is a type an instance?
Loading the hierarchy index…
Assumed by8
- ValuativeRel.uniformizer_pos
- ValuativeRel.IsNontrivial.condition
- ValuativeRel.IsNontrivial.exists_lt_one
- ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible
- Valuation.RankOne.ofRankLeOneStruct
- ValuativeRel.uniformizer_inv_le_iff
- instRankOneValueGroupWithZeroValuationOfIsNontrivialOfIsRankLeOne
- ValuativeRel.uniformizer_ne_zero
Ancestors0
No ancestors.