Structures · Algebra
ValuativeExtension
If B is an A algebra and both A and B have valuative relations,
we say that B|A is a valuative extension if the valuative relation on A is
induced by the one on B.
- Shape
- 2 explicit arguments · adds vle_iff_vle
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
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 by12
- ValuativeExtension.mapValueGroupWithZero
- ValuativeExtension.mapPosSubmonoid
- ValuativeExtension.mapValueGroupWithZero_strictMono
- ValuativeExtension.vle_iff_vle
- ValuativeExtension.mapPosSubmonoid_apply_coe
- ValuativeExtension.mapValueGroupWithZero_mk
- ValuativeExtension.mapValueGroupWithZero.congr_simp
- ValuativeExtension.mapValueGroupWithZero_valuation
- ValuativeExtension.mapPosSubmonoid.congr_simp
- ValuativeRel.IsRankLeOne.of_valuativeExtension
- ValuativeExtension.compatible_comap
- ValuativeExtension.vlt_iff_vlt
Ancestors0
No ancestors.