ValuedField

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

Statistics

Metric	Count
Definitions extension, extensionValuation, integer, maximalIdeal, valuedCompletion, «term𝒪[_]», «term𝓀[_]», «term𝓂[_]»	8
Theorems inversion_estimate, inversion_estimate', closure_coe_completion_v_lt, closure_coe_completion_v_mul_v_lt, completable, continuous_extension, continuous_extensionValuation, continuous_valuation, exists_coe_eq_v, extensionValuation_apply_coe, extension_eq_zero_iff, extension_extends, instFaithfulSMulCompletionOfUniformContinuousConstSMul, isTopologicalDivisionRing, valuation_isClosedMap, valuedCompletion_apply, valuedCompletion_surjective_iff, separated	18
Total	26

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	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	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	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	5 math math: continuous_extension, extension_extends, extension_eq_zero_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, FunctionField.valuedFqtInfty.def
extensionValuation 📖	CompOp	5 math math: exists_coe_eq_v, continuous_extensionValuation, closure_coe_completion_v_lt, closure_coe_completion_v_mul_v_lt, extensionValuation_apply_coe
integer 📖	CompOp	16 math math: integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, integer.exists_norm_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, integer.isUnit_iff_norm_eq_one, integer.isPrincipalIdealRing_of_compactSpace, integer.totallyBounded_iff_finite_residueField, integer.norm_coe_unit, integer.exists_norm_coe_lt_one
maximalIdeal 📖	CompOp	3 math math: integer.finite_quotient_maximalIdeal_pow_of_finite_residueField, Irreducible.maximalIdeal_eq_closedBall, Irreducible.maximalIdeal_pow_eq_closedBall_pow
valuedCompletion 📖	CompOp	16 math math: Padic.withValUniformEquiv_norm_le_one_iff, valuedCompletion_surjective_iff, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, Valuation.IsEquiv.valuedCompletion_le_one_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, 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.adicCompletionIntegers.isUnit_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, 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 ContinuousAt.preimage_mem_nhds Continuous.continuousAt continuous_extension WithZeroTopology.singleton_mem_nhds_of_ne_zero mem_closure_iff_nhds' extension_extends DenseRange.mem_nhds UniformSpace.Completion.denseRange_coe Filter.inter_mem eq_or_ne completable Valuation.zero_iff GroupWithZero.toNontrivial 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 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 GroupWithZero.toNontrivial 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 LinearOrderedCommMonoidWithZero.toIsOrderedMonoid mul_le_mul' covariant_swap_mul_of_covariant_mul le_refl
continuous_extension 📖	mathematical	—	Continuous UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace WithZeroTopology.topologicalSpace extension	—	IsDenseInducing.continuous_extend T4Space.t3Space T5Space.toT4Space WithZeroTopology.t5Space UniformSpace.Completion.isDenseInducing_coe eq_or_ne Topology.IsInducing.nhds_eq_comap IsDenseInducing.isInducing Continuous.tendsto' continuous_valuation map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Valuation.map_one zero_ne_one NeZero.one GroupWithZero.toNontrivial Set.ext Set.mem_preimage Set.mem_singleton_iff Set.mem_setOf_eq loc_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 Set.mem_compl_singleton_iff mul_assoc mul_inv_cancel₀ mul_one inv_mul_cancel₀ Continuous.fun_mul continuous_id' continuous_const Set.image_eq_preimage_of_inverse DenseRange.mem_nhds UniformSpace.Completion.denseRange_coe mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain Valuation.ne_zero_iff WithZeroTopology.tendsto_of_ne_zero Filter.eventually_comap Filter.mp_mem Filter.univ_mem' map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass UniformSpace.Completion.coe_mul mul_inv mul_comm Valuation.map_mul
continuous_extensionValuation 📖	mathematical	—	Continuous UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace WithZeroTopology.topologicalSpace DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup Valuation.instFunLike extensionValuation	—	continuous_extension
continuous_valuation 📖	mathematical	—	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 mem_nhds_zero subset_refl Set.instReflSubset Valuation.ne_zero_iff GroupWithZero.toNontrivial WithZeroTopology.tendsto_of_ne_zero loc_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 IsClosed.preimage continuous_extensionValuation 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	—	extension_extends
extension_eq_zero_iff 📖	mathematical	—	extension MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero UniformSpace.Completion toUniformSpace DivisionRing.toRing Field.toDivisionRing instZeroCompletion NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	IsTopologicalDivisionRing.toIsTopologicalRing isTopologicalDivisionRing toIsUniformAddGroup completable GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
extension_extends 📖	mathematical	—	extension UniformSpace.Completion.coe' toUniformSpace DivisionRing.toRing Field.toDivisionRing DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v	—	IsDenseInducing.extend_eq_of_tendsto T25Space.t2Space T3Space.t25Space T4Space.t3Space T5Space.toT4Space WithZeroTopology.t5Space UniformSpace.Completion.isDenseInducing_coe 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.IsTorsionFree.to_faithfulSMul IsTopologicalDivisionRing.toIsTopologicalRing IsDomain.toIsCancelMulZero instIsDomain IsSimpleRing.instNontrivial DivisionRing.isSimpleRing instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
isTopologicalDivisionRing 📖	mathematical	—	IsTopologicalDivisionRing UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing	—	instIsTopologicalRing mem_nhds Filter.mem_map Valuation.ne_zero_iff GroupWithZero.toNontrivial Valuation.inversion_estimate Units.val_mul Units.min_val
valuation_isClosedMap 📖	mathematical	—	IsClosedMap UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing Field.toDivisionRing WithZeroTopology.topologicalSpace DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v	—	IsClosedMap.of_nonempty GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass 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'	—	extension_extends
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 Set.ext 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 IsTopologicalRing.to_topologicalAddGroup IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.mem_nhds Valuation.ne_zero_iff GroupWithZero.toNontrivial sub_zero lt_irrefl T1Space.t0Space T2Space.t1Space

---

← Back to Index