Structures · Algebra
Valuation.Compatible
We say that a valuation v is Compatible if the relation x ≤ᵥ y
is equivalent to v x ≤ v y.
- Shape
- One type argument · adds vle_iff_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Padic
- WithVal
How is a type an instance?
Loading the hierarchy index…
Assumed by74
- ValuativeRel.ValueGroupWithZero.orderMonoidIso
- ValuativeRel.ValueGroupWithZero.embed
- ValuativeRel.isEquiv
- Valuation.mem_nhds_iff
- Valuation.isClosed_closedBall
- ValuativeRel.ValueGroupWithZero.embed_strictMono
- Valuation.isOpen_closedBall
- Valuation.Compatible.vle_iff_le
- Valuation.isClopen_sphere
- Valuation.isOpen_ball
- Valuation.vle_iff_le
- ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀
- ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀
- Valuation.isClopen_closedBall
- Valuation.isClosed_ball
- Valuation.isClopen_ball
- Valuation.isClosed_integer
- Valuation.vlt_iff_lt
- Valuation.isOpen_integer
- Valuation.exists_setOfPred_restrict_le_iff
- Valuation.toUniformSpace_eq
- ValuativeRel.subsingleton_units_valueGroupWithZero_of_trivialRel
- Valuation.mem_nhds_zero_iff
- Valuation.hasBasis_uniformity
- Valuation.isOpen_sphere
- Valuation.hasBasis_nhds_zero
- Valuation.isClopen_integer
- ValuativeRel.IsRankLeOne.of_compatible_mulArchimedean
- IsValuativeTopology.of_mem_nhds_iff_vle
- ValuativeRel.isNontrivial_iff_isNontrivial
- Valuation.discreteTopology_of_forall_map_eq_one
- ValuativeRel.ValueGroupWithZero.embed_mk
- Valuation.hasBasis_nhds
- Valuation.apply_posSubmonoid_ne_zero
- Valuation.is_topological_valuation
- ValuativeRel.eq_trivialRel_of_compatible_one
- ValuativeRel.valuation_lt_symm_orderMonoidIso
- Valuation.isClosed_sphere
- Padic.valuation_p_ne_zero
- ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono
- Valuation.isClopen_valuationSubring
- ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible
- Valuation.isOpen_valuationSubring
- ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk
- Valuation.veq_iff_eq
- IsValuativeTopology.isClopen_sphere
- Valuation.one_vle_iff
- IsValuativeTopology.isOpen_ball
- Valuation.cauchy_iff
- ValuativeRel.IsDiscrete.of_compatible_withZeroMulInt
Ancestors0
No ancestors.