Structures · Algebra
Valuation.RankOne
A valuation has rank one if it is nontrivial and its image is contained in ℝ≥0.
Note that this class includes the data of an inclusion morphism Γ₀ → ℝ≥0.
- Defined in
- Mathlib.RingTheory.Valuation.RankOne
- Shape
- One type argument
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- PadicComplex
- IsDedekindDomain.HeightOneSpectrum.adicCompletion
- PadicAlgCl
How is a type an instance?
Loading the hierarchy index…
Assumed by40
- Valuation.RankOne.hom
- Valued.toNormedField
- Valuation.RankOne.strictMono
- Valuation.norm
- Valued.toNormedField.setOfPred_mem_integer_eq_closedBall
- Valuation.norm_def
- Valued.toNormedField.norm_lt_one_iff
- Valuation.RankOne.unit
- Valuation.RankOne.nontrivial
- ValuativeRel.isRankLeOne_of_rankOne
- Valued.integer.totallyBounded_iff_finite_residueField
- Valuation.RankOne.exists_val_lt
- Valuation.norm_add_le
- Valuation.RankOne.zero_of_hom_zero
- Valued.toNormedField.one_lt_norm_iff
- Valued.coe_valuation_eq_rankOne_hom_comp_valuation
- Valuation.RankOne.hom_eq_zero_iff
- Valuation.RankOne.toIsNontrivial
- ValuativeRel.isNontrivial_of_rankOne
- Valued.toNormedField.one_le_norm_iff
- Valuation.RankOne.unit_ne_one
- Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField
- Valuation.RankOne.isNontrivial_restrict
- Valuation.norm_nonneg
- Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField
- Valued.integer.properSpace_iff_compactSpace_integer
- Valued.toNormedField.norm_le_one_iff
- Valued.toNormedField.norm_le_iff
- Valuation.RankOne.toRankLeOne
- Valued.toNormedField.norm_lt_iff
- Valued.instIsUltrametricDist
- Valued.toNontriviallyNormedField
- Valued.toNormedField.setOf_mem_integer_eq_closedBall
- Valued.toNormedField.norm_def
- Valuation.RankOne.instIsNontrivial
- Valuation.norm_pos_iff_valuation_pos
- Valued.isNonarchimedean_norm
- Valuation.RankOne.restrict_RankOne_hom_eq
- Valuation.norm_eq_zero
- Valuation.RankOne.restrict_RankOne