ValuationTopology

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

Statistics

Metric	Count
Definitions Valued, mk', toUniformSpace, v	4
Theorems map_eq_one_of_forall_lt, subgroups_basis, cauchy_iff, discreteTopology_of_forall_lt, discreteTopology_of_forall_map_eq_one, hasBasis_nhds_zero, hasBasis_uniformity, instIsTopologicalRing, isClopen_ball, isClopen_closedBall, isClopen_integer, isClopen_sphere, isClopen_valuationSubring, isClosed_ball, isClosed_closedBall, isClosed_integer, isClosed_sphere, isClosed_valuationSubring, isOpen_ball, isOpen_closedBall, isOpen_closedball, isOpen_integer, isOpen_sphere, isOpen_valuationSubring, is_topological_valuation, locally_const, mem_nhds, mem_nhds_zero, toIsUniformAddGroup, toUniformSpace_eq	30
Total	34

Valuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_eq_one_of_forall_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	CanLift.prf instCanLiftUnitsValIsUnit lt_trichotomy exists_pow_lt Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid Units.instMulArchimedean MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass LT.lt.not_gt map_pow isReduced_of_noZeroDivisors GroupWithZero.noZeroDivisors GroupWithZero.toNontrivial inv_lt_one' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toIsOrderedCancelMonoid IsOrderedMonoid.toMulLeftMono inv_pow Units.val_inv_eq_inv_val zpow_neg zpow_natCast map_inv₀
subgroups_basis 📖	mathematical	—	RingSubgroupsBasis Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup ltAddSubgroup DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map MonoidHomClass.toMonoidHom MonoidWithZeroHom WithZero.instMulZeroOneClass Monoid.toMulOneClass MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.embedding	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Monotone.map_inf StrictMono.monotone MonoidWithZeroHom.ValueGroup₀.embedding_strictMono Units.min_val exists_square_le IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toIsOrderedCancelMonoid Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid IsOrderedMonoid.toMulLeftMono restrict_lt_iff_lt_embedding map_mul mul_lt_mul'' LinearOrderedCommMonoidWithZero.toPosMulStrictMono MulPosStrictMono.toMulPosMono LinearOrderedCommMonoidWithZero.toMulPosStrictMono zero_le' GroupWithZero.eq_zero_or_unit MulZeroClass.zero_mul Units.zero_lt GroupWithZero.toNontrivial Units.val_inv_eq_inv_val map_inv₀ mul_comm inv_inv mul_inv_lt_of_lt_mul₀ SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass map_mul MonoidHomClass.toMulHomClass Units.val_mul MulZeroClass.mul_zero

Valued

Definitions

Name	Category	Theorems
mk' 📖	CompOp	1 math math: Valuation.IsEquiv.uniformContinuous
toUniformSpace 📖	CompOp	156 math math: continuous_extension, isOpen_closedball, IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, extension_extends, valuedCompletion_surjective_iff, IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap, PadicComplex.valuation_extends, PadicComplex.charZero, PadicComplex.coe_eq, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV, PadicComplex.norm_eq_norm, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, NumberField.FinitePlace.norm_def', IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, NumberField.FinitePlace.embedding_apply, toUniformSpace_eq, NumberField.HeightOneSpectrum.rankOne_hom'_def, Valuation.IsEquiv.valuedCompletion_le_one_iff, PadicComplex.coe_natCast, isClopen_ball, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', Valuation.IsEquiv.uniformContinuous_equiv, exists_coe_eq_v, NumberField.FinitePlace.norm_embedding_eq, LaurentSeries.inducing_coe, LaurentSeries.continuous_coe, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, is_topological_valuation, continuous_valuation, NumberField.FinitePlace.norm_embedding, extension_eq_zero_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, tendsto_zero_pow_of_le_exp_neg_one, FunctionField.valuedFqtInfty.def, isClopen_valuationSubring, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, tendsto_zero_pow_of_v_lt_one, isOpen_sphere, isClosed_valuationSubring, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, Valuation.IsEquiv.uniformContinuous_equivWithVal, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_1, instIsTopologicalRing, hasBasis_nhds_zero, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, toIsUniformAddGroup, discreteTopology_of_forall_lt, NumberField.FinitePlace.norm_lt_one_iff_mem, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', isClosed_ball, PadicAlgCl.instUniformContinuousConstSMulPadic, Valuation.IsEquiv.uniformContinuous_congr, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, isClopen_sphere, PadicComplex.valuation_p, isClosed_sphere, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, ValuedRing.separated, PadicComplex.norm_extends', NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, PadicComplex.isNonarchimedean, isOpen_valuationSubring, PadicInt.coe_adicCompletionIntegersEquiv_apply, locally_const, LaurentSeries.coe_X_compare, NumberField.HeightOneSpectrum.embedding_mul_absNorm, closure_coe_completion_v_lt, valuation_isClosedMap, closure_coe_completion_v_mul_v_lt, valuedCompletion_apply, cauchy_iff, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.continuous_coe', NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply, NumberField.FinitePlace.norm_def_int, isClosed_integer, integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, PadicComplex.instIsScalarTowerPadicPadicAlgCl, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, isClopen_integer, LaurentSeries.valuation_LaurentSeries_equal_extension, PadicComplex.norm_eq_norm', LaurentSeries.LaurentSeries_coe, LaurentSeries.powerSeries_ext_subring, NumberField.HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, PadicComplex.coe_zero, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, integer.properSpace_iff_compactSpace_integer, isOpen_closedBall, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, mem_nhds_zero, isOpen_ball, mem_nhds, extensionValuation_apply_coe, LaurentSeries.instLaurentSeriesComplete, discreteTopology_of_forall_map_eq_one, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, PadicComplex.RankOne.hom_eq_embedding, NumberField.FinitePlace.norm_eq_one_iff_notMem, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, isOpen_integer, LaurentSeries.tendsto_valuation, PadicComplex.norm_extends, LaurentSeries.coe_range_dense, completable, Valuation.IsEquiv.uniformContinuous_equiv_symm, Padic.coe_withValRingEquiv_symm, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, LaurentSeries.comparePkg_eq_extension, hasBasis_uniformity, Valuation.IsEquiv.uniformContinuous, instFaithfulSMulCompletionOfUniformContinuousConstSMul, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, LaurentSeries.uniformContinuous_coeff, isClosed_closedBall, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, integer.totallyBounded_iff_finite_residueField, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, PadicComplex.nnnorm_extends', continuous_valuation_of_surjective, NumberField.FinitePlace.norm_embedding', NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, isClopen_closedBall, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, PadicComplex.nnnorm_extends, NumberField.FinitePlace.norm_embedding_int, isTopologicalDivisionRing, Padic.isDenseInducing_cast_withVal, LaurentSeries.uniformContinuous_withVal_equiv, PadicComplexInt.integers, NumberField.FinitePlace.norm_def, PadicComplex.isAlgClosed, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, extensionValuation_toFun
v 📖	CompOp	116 math math: continuous_extension, isOpen_closedball, WithVal.valued_toVal, WithVal.valueGroupOrderIso₀_symm_apply, Padic.withValUniformEquiv_norm_le_one_iff, toNormedField.norm_le_one_iff, extension_extends, WithVal.valueGroup_eq, valuedCompletion_surjective_iff, PadicComplex.valuation_extends, NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV, PadicComplex.norm_eq_norm, WithVal.valueGroupOrderIso₀_restrict, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, WithVal.apply_ofVal, WithVal.valueGroupOrderIso₀_apply, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, LaurentSeries.valuation_single_zpow, toUniformSpace_eq, NumberField.HeightOneSpectrum.rankOne_hom'_def, WithVal.valueGroupEquiv_symm_apply, Valuation.IsEquiv.valuedCompletion_le_one_iff, isClopen_ball, exists_coe_eq_v, is_topological_valuation, continuous_valuation, WithVal.apply_symm_equiv, LaurentSeries.val_le_one_iff_eq_coe, extension_eq_zero_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, WithVal.val_apply_equiv, FunctionField.valuedFqtInfty.def, isClopen_valuationSubring, WithVal.apply_equiv, isOpen_sphere, isClosed_valuationSubring, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, LaurentSeries.exists_ratFunc_val_lt, hasBasis_nhds_zero, WithVal.strictMono_valueGroupOrderIso₀, WithVal.strictMono_valueGroupOrderIso₀_symm, RatFunc.valuation_surjective, WithVal.valueGroupEquiv_apply, coe_valuation_eq_rankOne_hom_comp_valuation, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', isClosed_ball, isClopen_sphere, PadicAlgCl.valuation_p, PadicComplex.valuation_p, isClosed_sphere, isOpen_valuationSubring, locally_const, toNormedField.norm_le_iff, integer.mulArchimedean_mrange_of_isCompact_integer, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, closure_coe_completion_v_lt, valuation_isClosedMap, closure_coe_completion_v_mul_v_lt, valuedCompletion_apply, cauchy_iff, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, isClosed_integer, toNormedField.one_lt_norm_iff, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, WithVal.strictMono_valueGroupEquiv_symm, isClopen_integer, LaurentSeries.valuation_LaurentSeries_equal_extension, PadicComplex.norm_eq_norm', RatFunc.v_def, PadicAlgCl.valuation_def, PadicAlgCl.valuation_coe, FunctionField.inftyValuedFqt.def, isOpen_closedBall, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, mem_nhds_zero, isOpen_ball, NormedField.v_eq_valuation, mem_nhds, integer.locallyFiniteOrder_units_mrange_of_isCompact_integer, extensionValuation_apply_coe, LaurentSeries.valuation_surjective, LaurentSeries.valuation_coe_ratFunc, PadicComplex.RankOne.hom_eq_embedding, WithVal.valueGroupOrderIso₀_symm_restrict, LaurentSeries.valuation_compare, isOpen_integer, toNormedField.norm_def, LaurentSeries.tendsto_valuation, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', IsValuativeTopology.v_eq_valuation, toNormedField.norm_lt_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, hasBasis_uniformity, LaurentSeries.valuation_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, toNormedField.setOf_mem_integer_eq_closedBall, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, IsNonarchimedeanLocalField.instCompatibleValueGroupWithZeroV, isClosed_closedBall, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, continuous_valuation_of_surjective, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, isClopen_closedBall, WithVal.strictMono_valueGroupEquiv, exists_pow_lt_of_le_exp_neg_one, toNormedField.norm_lt_one_iff, LaurentSeries.exists_ratFunc_eq_v, toNormedField.one_le_norm_iff, PadicComplexInt.integers, LaurentSeries.valuation_X_pow, NumberField.FinitePlace.norm_def, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, extensionValuation_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchy_iff 📖	mathematical	—	Cauchy toUniformSpace Filter.NeBot Set Filter Filter.instMembership MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val WithZero.instMonoidWithZero DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHomClass.toMonoidHomClass Valuation.subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup toUniformSpace_eq AddGroupFilterBasis.cauchy_iff RingSubgroupsBasis.mem_addGroupFilterBasis_iff RingSubgroupsBasis.mem_addGroupFilterBasis
discreteTopology_of_forall_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing Valuation.instFunLike v	DiscreteTopology UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing	—	discreteTopology_of_forall_map_eq_one GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Valuation.map_eq_one_of_forall_lt
discreteTopology_of_forall_map_eq_one 📖	mathematical	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	DiscreteTopology UniformSpace.toTopologicalSpace toUniformSpace	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRing Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq LT.lt.ne map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass Units.val_one Valuation.restrict_lt_iff_lt_embedding
hasBasis_nhds_zero 📖	mathematical	—	Filter.HasBasis Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup nhds UniformSpace.toTopologicalSpace toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict Units.val	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass
hasBasis_uniformity 📖	mathematical	—	Filter.HasBasis Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup uniformity toUniformSpace setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass uniformity_eq_comap_nhds_zero IsUniformAddGroup.isRightUniformAddGroup toIsUniformAddGroup Filter.HasBasis.comap hasBasis_nhds_zero
instIsTopologicalRing 📖	mathematical	—	IsTopologicalRing UniformSpace.toTopologicalSpace toUniformSpace NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup RingFilterBasis.isTopologicalRing toUniformSpace_eq
isClopen_ball 📖	mathematical	—	IsClopen UniformSpace.toTopologicalSpace toUniformSpace setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass isClosed_ball isOpen_ball
isClopen_closedBall 📖	mathematical	—	IsClopen UniformSpace.toTopologicalSpace toUniformSpace setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 Preorder.toLE WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass isClosed_closedBall isOpen_closedBall
isClopen_integer 📖	mathematical	—	IsClopen UniformSpace.toTopologicalSpace toUniformSpace SetLike.coe Subring Ring.toNonAssocRing Subring.instSetLike Valuation.integer v	—	isClosed_integer isOpen_integer
isClopen_sphere 📖	mathematical	—	IsClopen UniformSpace.toTopologicalSpace toUniformSpace setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Set.ext IsClopen.diff isClopen_closedBall isClopen_ball
isClopen_valuationSubring 📖	mathematical	—	IsClopen UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing Field.toDivisionRing SetLike.coe ValuationSubring ValuationSubring.instSetLike Valuation.valuationSubring v	—	isClopen_integer
isClosed_ball 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace toUniformSpace setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass eq_or_ne AddSubgroup.isClosed_of_isOpen instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRing isOpen_ball
isClosed_closedBall 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace toUniformSpace setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 Preorder.toLE WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass isOpen_compl_iff isOpen_iff_mem_nhds mem_nhds ne_of_gt lt_of_le_of_lt zero_le' ne_of_lt Valuation.map_sub_eq_of_lt_left Valuation.map_sub_swap
isClosed_integer 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace toUniformSpace SetLike.coe Subring Ring.toNonAssocRing Subring.instSetLike Valuation.integer v	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.restrict_le_one_iff isClosed_closedBall
isClosed_sphere 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace toUniformSpace setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass eq_or_ne isClosed_closedBall IsClopen.isClosed isClopen_sphere
isClosed_valuationSubring 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing Field.toDivisionRing SetLike.coe ValuationSubring ValuationSubring.instSetLike Valuation.valuationSubring v	—	isClosed_integer
isOpen_ball 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass isOpen_iff_mem_nhds eq_or_ne nhds_neBot mem_nhds LE.le.trans_lt Valuation.map_add max_lt sub_add_cancel
isOpen_closedBall 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 Preorder.toLE WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass isOpen_iff_mem_nhds mem_nhds le_trans Valuation.map_add max_le le_of_lt sub_add_cancel
isOpen_closedball 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 Preorder.toLE WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	isOpen_closedBall
isOpen_integer 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace SetLike.coe Subring Ring.toNonAssocRing Subring.instSetLike Valuation.integer v	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.restrict_le_one_iff isOpen_closedBall one_ne_zero NeZero.one WithZero.instNontrivial One.instNonempty
isOpen_sphere 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring 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 DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass IsClopen.isOpen MonoidWithZeroHom.monoidWithZeroHomClass isClopen_sphere
isOpen_valuationSubring 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing Field.toDivisionRing SetLike.coe ValuationSubring ValuationSubring.instSetLike Valuation.valuationSubring v	—	isOpen_integer
is_topological_valuation 📖	mathematical	—	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Set.instHasSubset setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict Units.val	—	—
locally_const 📖	mathematical	—	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace toUniformSpace setOf DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass mem_nhds Units.val_mk0 Valuation.map_eq_of_sub_lt Valuation.restrict_lt_iff
mem_nhds 📖	mathematical	—	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace toUniformSpace Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Set.instHasSubset setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass nhds_translation_add_neg IsUniformAddGroup.to_topologicalAddGroup toIsUniformAddGroup Filter.HasBasis.mem_iff Filter.HasBasis.comap hasBasis_nhds_zero
mem_nhds_zero 📖	mathematical	—	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Set.instHasSubset setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict Units.val	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass sub_zero
toIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup toUniformSpace AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	—
toUniformSpace_eq 📖	mathematical	—	toUniformSpace IsTopologicalAddGroup.rightUniformSpace AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne RingSubgroupsBasis.topology Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Units.instInhabited Valuation.ltAddSubgroup DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map MonoidHomClass.toMonoidHom MonoidWithZeroHom WithZero.instMulZeroOneClass Monoid.toMulOneClass MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.embedding Valuation.subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup RingFilterBasis.toAddGroupFilterBasis RingSubgroupsBasis.toRingFilterBasis	—	UniformSpace.ext ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup Filter.HasBasis.eq_of_same_basis hasBasis_uniformity sub_eq_add_neg Filter.HasBasis.comap RingSubgroupsBasis.hasBasis_nhds_zero

(root)

Definitions

Name	Category	Theorems
Valued 📖	CompData	—

---

← Back to Index