Structures · Topology
Valued
A valued ring is a ring that comes equipped with a distinguished valuation. The class Valued
is designed for the situation that there is a canonical valuation on the ring.
TODO: show that there always exists an equivalent valuation taking values in a type belonging to
the same universe as the ring.
See Note [forgetful inheritance] for why we extend UniformSpace, IsUniformAddGroup.
- Shape
- 2 explicit arguments · adds v, is_topological_valuation
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances9
- RatFunc
- UniformSpace.Completion
- PadicComplex
- IsDedekindDomain.HeightOneSpectrum.adicCompletion
- PadicAlgCl
- WithVal
- RatFunc.CompletionAtInfty
- AbstractCompletion.space
- LaurentSeries
How is a type an instance?
Loading the hierarchy index…
Assumed by84
- Valued.v
- Valued.integer
- Valued.toNormedField
- Valued.valuedCompletion_apply
- Valued.extensionValuation
- Valued.extension
- Valued.mem_nhds
- Valued.hasBasis_nhds_zero
- Valued.isClosed_closedBall
- Valued.maximalIdeal
- Valued.hasBasis_uniformity
- Valued.ResidueField
- Valued.extensionValuation_apply_coe
- Valued.isClopen_closedBall
- Valued.isOpen_closedBall
- Valued.locally_const
- Valued.mem_nhds_zero
- Valued.toNormedField.setOfPred_mem_integer_eq_closedBall
- Valuation.IsEquiv.uniformContinuous_equiv
- Valued.isOpen_ball
- Valued.valuedCompletion_surjective_iff
- Valued.continuous_valuation
- Valued.continuous_extension
- Valued.isOpen_integer
- Valued.isClopen_sphere
- Valued.extension_extends
- Valued.continuous_valuation_of_surjective
- Valued.isOpen_sphere
- Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer
- Valued.isClosed_integer
- Valued.integer.isDiscreteValuationRing_of_compactSpace
- Valuation.IsEquiv.uniformContinuous_equiv_symm
- Valued.toNormedField.norm_lt_one_iff
- Valued.valuation_isClosedMap
- Valued.toUniformSpace_eq
- Valued.closure_coe_completion_v_lt
- Valued.isClopen_ball
- Valued.integer.mulArchimedean_mrange_of_isCompact_integer
- Valued.integer.totallyBounded_iff_finite_residueField
- Valued.integer.isPrincipalIdealRing_of_compactSpace
- Valued.isClopen_integer
- Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField
- Valued.tendsto_zero_pow_of_v_lt_one
- Valued.isClosed_ball
- Valued.discreteTopology_of_forall_map_eq_one
- Valued.is_topological_valuation
- Valued.toNormedField.one_lt_norm_iff
- Valued.coe_valuation_eq_rankOne_hom_comp_valuation
- Valued.instIsTopologicalRing
- Valued.isOpen_valuationSubring