ValuedField

📁 Source: Mathlib/Topology/Algebra/Valued/ValuedField.lean

Statistics

Metric	Count
Definitions extension, extensionValuation, instLinearOrderedCommGroupWithZeroValueGroup₀ValuationV, integer, maximalIdeal, valueGroup₀_equiv_extensionValuation, valueGroup₀_hom_extensionValuation, valuedCompletion, «term𝒪[_]», «term𝓀[_]», «term𝓂[_]»	11
Theorems inversion_estimate, inversion_estimate', closure_coe_completion_v_lt, closure_coe_completion_v_mul_v_lt, completable, continuous_extension, continuous_valuation, continuous_valuation_of_surjective, exists_coe_eq_v, extensionValuation_apply_coe, extensionValuation_toFun, extension_eq_zero_iff, extension_extends, instFaithfulSMulCompletionOfUniformContinuousConstSMul, isTopologicalDivisionRing, valuation_isClosedMap, valuedCompletion_apply, valuedCompletion_surjective_iff, separated	19
Total	30

Valuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion_estimate 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SemilatticeInf.toMin MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Units.val MonoidWithZero.toMonoid	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	lt_of_lt_of_le min_le_left mul_inv_lt_of_lt_mul₀ min_le_right map_eq_of_sub_lt zero_iff GroupWithZero.toNontrivial map_zero mul_sub_left_distrib sub_mul mul_assoc mul_inv_cancel₀ inv_mul_cancel₀ mul_one one_mul map_mul map_inv₀ ValuationClass.toMonoidWithZeroHomClass instValuationClass mul_comm mul_inv_rev map_sub_swap
inversion_estimate' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SemilatticeInf.toMin MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass instValuationClass mul_lt_mul_of_pos_right LinearOrderedCommMonoidWithZero.toMulPosStrictMono inversion_estimate div_mul_cancel₀

Valued

Definitions

Name	Category	Theorems
extension 📖	CompOp	4 math math: continuous_extension, extension_extends, extension_eq_zero_iff, extensionValuation_toFun
extensionValuation 📖	CompOp	7 math math: exists_coe_eq_v, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, FunctionField.valuedFqtInfty.def, closure_coe_completion_v_lt, closure_coe_completion_v_mul_v_lt, extensionValuation_apply_coe, extensionValuation_toFun
instLinearOrderedCommGroupWithZeroValueGroup₀ValuationV 📖	CompOp	1 math math: continuous_extension
integer 📖	CompOp	20 math math: integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, integer.exists_norm_lt_one, integer.norm_irreducible_lt_one, integer.norm_le_one, integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, integer.coe_span_singleton_eq_closedBall, integer.isDiscreteValuationRing_of_compactSpace, integer.norm_unit, integer.exists_nnnorm_lt_one, integer.properSpace_iff_compactSpace_integer, integer.finite_quotient_maximalIdeal_pow_of_finite_residueField, integer.mem_iff, Irreducible.maximalIdeal_eq_closedBall, integer.isUnit_iff_norm_eq_one, integer.isPrincipalIdealRing_of_compactSpace, Irreducible.maximalIdeal_pow_eq_closedBall_pow, integer.totallyBounded_iff_finite_residueField, integer.norm_coe_unit, integer.exists_norm_coe_lt_one, integer.norm_irreducible_pos
maximalIdeal 📖	CompOp	3 math math: integer.finite_quotient_maximalIdeal_pow_of_finite_residueField, Irreducible.maximalIdeal_eq_closedBall, Irreducible.maximalIdeal_pow_eq_closedBall_pow
valueGroup₀_equiv_extensionValuation 📖	CompOp	—
valueGroup₀_hom_extensionValuation 📖	CompOp	—
valuedCompletion 📖	CompOp	21 math math: Padic.withValUniformEquiv_norm_le_one_iff, valuedCompletion_surjective_iff, NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, NumberField.HeightOneSpectrum.rankOne_hom'_def, Valuation.IsEquiv.valuedCompletion_le_one_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', valuedCompletion_apply, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, LaurentSeries.valuation_compare, LaurentSeries.tendsto_valuation, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, NumberField.FinitePlace.norm_def, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers
«term𝒪[_]» 📖	CompOp	—
«term𝓀[_]» 📖	CompOp	—
«term𝓂[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_coe_completion_v_lt 📖	mathematical	—	closure UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace Set.image UniformSpace.Completion.coe' setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup extensionValuation	—	Set.ext IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass GroupWithZero.toNontrivial MonoidWithZeroHom.monoidWithZeroHomClass ContinuousAt.preimage_mem_nhds Continuous.continuousAt continuous_extension WithZeroTopology.singleton_mem_nhds_of_ne_zero mem_closure_iff_nhds' MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ extension_extends Valuation.restrict_def DenseRange.mem_nhds UniformSpace.Completion.denseRange_coe Filter.inter_mem eq_or_ne completable Valuation.zero_iff Valuation.map_zero subset_closure
closure_coe_completion_v_mul_v_lt 📖	mathematical	—	closure UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace Set.image UniformSpace.Completion.coe' setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation Valuation.instFunLike v UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup extensionValuation	—	GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono closure_coe_completion_v_lt
completable 📖	mathematical	—	CompletableTopField toUniformSpace DivisionRing.toRing Field.toDivisionRing	—	ValuedRing.separated ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Filter.inf_eq_bot_iff mem_nhds_zero le_of_not_gt cauchy_iff Filter.NeBot.map Filter.mem_map Filter.mem_of_superset Filter.inter_mem Set.subset_preimage_image Valuation.inversion_estimate WithZero.instNontrivial One.instNonempty Valuation.ne_zero_iff lt_of_lt_of_le Units.min_val mul_assoc Units.val_mul le_imp_le_of_le_of_le inf_le_inf mul_le_mul_right IsOrderedMonoid.toMulLeftMono MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid mul_le_mul' covariant_swap_mul_of_covariant_mul SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass le_refl
continuous_extension 📖	mathematical	—	Continuous UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace WithZeroTopology.topologicalSpace instLinearOrderedCommGroupWithZeroValueGroup₀ValuationV extension	—	IsDenseInducing.continuous_extend ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass T4Space.t3Space T5Space.toT4Space WithZeroTopology.t5Space UniformSpace.Completion.isDenseInducing_coe eq_or_ne UniformSpace.Completion.coe_zero Topology.IsInducing.nhds_eq_comap IsDenseInducing.isInducing Continuous.tendsto' MonoidWithZeroHom.monoidWithZeroHomClass continuous_valuation map_zero MonoidWithZeroHomClass.toZeroHomClass Valuation.map_one zero_ne_one NeZero.one GroupWithZero.toNontrivial Set.ext Set.mem_preimage Set.mem_singleton_iff Set.mem_setOf_eq locally_const Filter.mem_comap IsDenseInducing.nhds_eq_comap nhds_prod_eq isTopologicalDivisionRing completable toIsUniformAddGroup one_mul Filter.Tendsto.mul UniformSpace.Completion.instContinuousMul IsTopologicalDivisionRing.toIsTopologicalRing Continuous.continuousAt continuous_fst Filter.Tendsto.comp inv_one ContinuousAt.tendsto ContinuousInv₀.continuousAt_inv₀ IsTopologicalDivisionRing.toContinuousInv₀ UniformSpace.Completion.instIsTopologicalDivisionRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing continuous_snd Filter.tendsto_prod_self_iff compl_singleton_mem_nhds T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.Completion.t0Space UniformSpace.to_regularSpace Filter.inter_mem mul_assoc mul_inv_cancel₀ mul_one inv_mul_cancel₀ Continuous.mul_const IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing UniformSpace.Completion.topologicalRing continuous_id' Set.image_eq_preimage_of_inverse DenseRange.mem_nhds UniformSpace.Completion.denseRange_coe mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain Valuation.ne_zero_iff WithZero.instNontrivial One.instNonempty WithZeroTopology.tendsto_of_ne_zero Filter.eventually_comap Filter.mp_mem Filter.univ_mem' Valuation.restrict_def MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_one_iff map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass UniformSpace.Completion.coe_mul mul_inv mul_comm Valuation.map_mul
continuous_valuation 📖	mathematical	—	Continuous MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass v Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass UniformSpace.toTopologicalSpace toUniformSpace WithZeroTopology.topologicalSpace MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DFunLike.coe Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass continuous_iff_continuousAt eq_or_ne ContinuousAt.eq_1 map_zero MonoidWithZeroHomClass.toZeroHomClass WithZeroTopology.tendsto_zero Filter.Eventually.eq_1 mem_nhds_zero subset_refl Set.instReflSubset Valuation.ne_zero_iff WithZero.instNontrivial One.instNonempty WithZeroTopology.tendsto_of_ne_zero locally_const GroupWithZero.toNontrivial
continuous_valuation_of_surjective 📖	mathematical	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Valuation.instFunLike v	Continuous UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing WithZeroTopology.topologicalSpace DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v	—	continuous_iff_continuousAt eq_or_ne ContinuousAt.eq_1 map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithZeroTopology.tendsto_zero Filter.Eventually.eq_1 MonoidWithZeroHom.monoidWithZeroHomClass mem_nhds_zero Valuation.restrict_def Valuation.ne_zero_iff GroupWithZero.toNontrivial WithZeroTopology.tendsto_of_ne_zero locally_const
exists_coe_eq_v 📖	mathematical	—	DFunLike.coe Valuation UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace isTopologicalDivisionRing toIsUniformAddGroup Valuation.instFunLike extensionValuation v	—	IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup eq_or_ne extensionValuation_apply_coe DenseRange.induction_on UniformSpace.Completion.denseRange_coe ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ StrictMono.injective MonoidWithZeroHom.ValueGroup₀.embedding_strictMono MonoidWithZeroHom.monoidWithZeroHomClass IsClosed.preimage continuous_extension IsClosedMap.isClosed_range valuation_isClosedMap
extensionValuation_apply_coe 📖	mathematical	—	DFunLike.coe Valuation UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace isTopologicalDivisionRing toIsUniformAddGroup Valuation.instFunLike extensionValuation UniformSpace.Completion.coe' v	—	IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass extensionValuation_toFun MonoidWithZeroHom.monoidWithZeroHomClass extension_extends Valuation.restrict_def MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
extensionValuation_toFun 📖	mathematical	—	DFunLike.coe Valuation UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace isTopologicalDivisionRing toIsUniformAddGroup Valuation.instFunLike extensionValuation MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ v Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHom.ValueGroup₀.embedding extension	—	IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup
extension_eq_zero_iff 📖	mathematical	—	extension MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike v Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithZero.instZero Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup UniformSpace.Completion toUniformSpace instZeroCompletion MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup completable Valuation.zero_iff GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass
extension_extends 📖	mathematical	—	extension UniformSpace.Completion.coe' toUniformSpace DivisionRing.toRing Field.toDivisionRing DFunLike.coe Valuation MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass v Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	IsDenseInducing.extend_eq_of_tendsto ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass T25Space.t2Space T3Space.t25Space T4Space.t3Space T5Space.toT4Space WithZeroTopology.t5Space UniformSpace.Completion.isDenseInducing_coe MonoidWithZeroHom.monoidWithZeroHomClass IsDenseInducing.nhds_eq_comap Continuous.continuousAt continuous_valuation
instFaithfulSMulCompletionOfUniformContinuousConstSMul 📖	mathematical	—	FaithfulSMul UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing UniformSpace.Completion.instSMul Algebra.toSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	isTopologicalDivisionRing completable toIsUniformAddGroup faithfulSMul_iff_algebraMap_injective FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Ring.uniformContinuousConstSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing Module.Free.of_divisionRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing
isTopologicalDivisionRing 📖	mathematical	—	IsTopologicalDivisionRing UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing	—	instIsTopologicalRing ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass mem_nhds Filter.mem_map Valuation.ne_zero_iff WithZero.instNontrivial One.instNonempty Valuation.inversion_estimate Units.min_val
valuation_isClosedMap 📖	mathematical	—	IsClosedMap MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass v Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass UniformSpace.toTopologicalSpace toUniformSpace WithZeroTopology.topologicalSpace MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe Valuation.restrict	—	IsClosedMap.of_nonempty ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass WithZero.instNontrivial One.instNonempty Units.ne_zero HasSubset.Subset.trans Set.instIsTransSubset sub_zero em
valuedCompletion_apply 📖	mathematical	—	DFunLike.coe Valuation UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace isTopologicalDivisionRing toIsUniformAddGroup Valuation.instFunLike v valuedCompletion UniformSpace.Completion.coe'	—	IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ MonoidWithZeroHom.monoidWithZeroHomClass extension_extends Valuation.restrict_def
valuedCompletion_surjective_iff 📖	mathematical	—	UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace isTopologicalDivisionRing toIsUniformAddGroup Valuation.instFunLike v valuedCompletion	—	IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup UniformSpace.Completion.induction_on eq_or_ne GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass completable MonoidWithZeroHom.monoidWithZeroHomClass StrictMono.injective MonoidWithZeroHom.ValueGroup₀.embedding_strictMono MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ map_zero MonoidWithZeroHomClass.toZeroHomClass Set.ext Valuation.restrict_def IsClosed.sdiff isClosed_univ isOpen_sphere valuedCompletion_apply

ValuedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
separated 📖	mathematical	—	T0Space UniformSpace.toTopologicalSpace Valued.toUniformSpace DivisionRing.toRing	—	IsTopologicalAddGroup.t2Space_of_zero_sep IsSemitopologicalRing.toIsTopologicalAddGroup IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Valued.mem_nhds Valuation.ne_zero_iff WithZero.instNontrivial One.instNonempty sub_zero MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ lt_irrefl T1Space.t0Space T2Space.t1Space

---

← Back to Index