Structures · Algebra
ValuativeRel
The class [ValuativeRel R] class introduces an operator x ≤ᵥ y : Prop for x y : R
which is the natural relation arising from (the equivalence class of) a valuation on R when R
is a ring. More precisely, if v is a valuation on R then the associated relation is
x ≤ᵥ y ↔ v x ≤ v y. Use this class to talk about the case where R is equipped
with an equivalence class of valuations.
- Shape
- One type argument · adds vle, vle_total, vle_trans, vle_add, mul_vle_mul_left, vle_mul_cancel, not_vle_one_zero, vle_mul_comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Padic
- WithVal
- ValuativeRel.WithPreorder
How is a type an instance?
Loading the hierarchy index…
Assumed by299
- ValuativeRel.ValueGroupWithZero
- ValuativeRel.vle
- ValuativeRel.vlt
- ValuativeRel.posSubmonoid
- ValuativeRel.valuation
- ValuativeRel.veq
- ValuativeRel.ValueGroupWithZero.orderMonoidIso
- ValuativeRel.ValueGroupWithZero.embed
- ValuativeRel.ValueGroupWithZero.lift
- ValuativeRel.mul_vle_mul_left
- ValuativeRel.uniformizer
- ValuativeRel.ValueGroupWithZero.ind
- ValuativeRel.isEquiv
- Valuation.mem_nhds_iff
- ValuativeRel.mul_vle_mul_iff_left
- ValuativeExtension.mapValueGroupWithZero
- ValuativeRel.mul_vle_mul_right
- ValuativeRel.vle_total
- ValuativeRel.vle_refl
- ValuativeRel.veq_refl
- ValuativeRel.vle.trans_vlt
- ValuativeRel.vle_trans
- ValuativeRel.not_vle
- ValuativeRel.veq_mul_comm
- ValuativeRel.veq.vle
- ValuativeRel.vle.trans
- ValuativeExtension.mapPosSubmonoid
- ValuativeRel.vlt.trans_vle
- Valuation.isClosed_closedBall
- ValuativeRel.ValueGroupWithZero.embed_strictMono
- Valuation.isOpen_closedBall
- ValuativeRel.ValueGroupWithZero.sound
- ValuativeRel.supp
- Valuation.isClopen_sphere
- Valuation.isOpen_ball
- ValuativeRel.ValueGroupWithZero.mk_eq_div
- Valuation.vle_iff_le
- ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀
- ValuativeRel.mul_vlt_mul_left
- ValuativeRel.not_vlt
- ValuativeRel.valuation_eq_zero_iff
- ValuativeRel.mul_vle_mul
- ValuativeRel.vle.not_vlt
- ValuativeRel.vle.rfl
- ValuativeRel.veq_comm
- ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀
- ValuativeRel.ValueGroupWithZero.mk_eq_zero
- ValuativeRel.posSubmonoid_def
- ValuativeRel.vlt.vle
- ValuativeRel.mul_vle_mul_iff_right
Ancestors0
No ancestors.