WithAbs

📁 Source: Mathlib/Analysis/Normed/Field/WithAbs.lean

Statistics

Metric	Count
Definitions extensionEmbedding_of_comp, instCoe, instField, normedField	4
Theorems extensionEmbedding_dist_eq_of_comp, extensionEmbedding_of_comp_coe, isClosedEmbedding_extensionEmbedding_of_comp, isometry_extensionEmbedding_of_comp, locallyCompactSpace, instFiniteDimensional, instIsSeparable, isUniformInducing_of_comp, isometry_of_comp, pseudoMetricSpace_induced_of_comp, tendsto_one_div_one_add_pow_nhds_one, uniformSpace_comap_eq_of_comp	12
Total	16

AbsoluteValue.Completion

Definitions

Name	Category	Theorems
extensionEmbedding_of_comp 📖	CompOp	—
instCoe 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extensionEmbedding_dist_eq_of_comp 📖	mathematical	Norm.norm NormedField.toNorm DFunLike.coe RingHom WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semiring.toNonAssocSemiring WithAbs.instSemiring NormedField.toField RingHom.instFunLike AbsoluteValue AbsoluteValue.funLike	Dist.dist PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing WithAbs.normedField Ring.toSemiring UniformSpace.Completion.ring WithAbs.instRing DivisionRing.toRing Field.toDivisionRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing UniformSpace.toTopologicalSpace NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup NormedRing.toRing NormedCommRing.toNormedRing Isometry.extensionHom CompletableTopField.toT0Space completableTopField_of_complete T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass AbsoluteValue.Completion UniformSpace.Completion.instDist	—	Isometry.dist_eq Isometry.completion_extension CompletableTopField.toT0Space completableTopField_of_complete NormedDivisionRing.to_isTopologicalDivisionRing T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
extensionEmbedding_of_comp_coe 📖	mathematical	Norm.norm NormedField.toNorm DFunLike.coe RingHom WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semiring.toNonAssocSemiring WithAbs.instSemiring NormedField.toField RingHom.instFunLike AbsoluteValue AbsoluteValue.funLike	UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField Ring.toSemiring UniformSpace.Completion.ring WithAbs.instRing DivisionRing.toRing Field.toDivisionRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing UniformSpace.toTopologicalSpace NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup NormedRing.toRing NormedCommRing.toNormedRing Isometry.extensionHom CompletableTopField.toT0Space SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing completableTopField_of_complete T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass UniformSpace.Completion.coe'	—	Isometry.extensionHom_coe IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup CompletableTopField.toT0Space completableTopField_of_complete T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
isClosedEmbedding_extensionEmbedding_of_comp 📖	mathematical	Norm.norm NormedField.toNorm DFunLike.coe RingHom WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semiring.toNonAssocSemiring WithAbs.instSemiring NormedField.toField RingHom.instFunLike AbsoluteValue AbsoluteValue.funLike	Topology.IsClosedEmbedding UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Ring.toSemiring UniformSpace.Completion.ring WithAbs.instRing DivisionRing.toRing Field.toDivisionRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup NormedRing.toRing NormedCommRing.toNormedRing Isometry.extensionHom CompletableTopField.toT0Space completableTopField_of_complete T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass	—	Isometry.isClosedEmbedding UniformSpace.Completion.completeSpace Isometry.completion_extension CompletableTopField.toT0Space completableTopField_of_complete NormedDivisionRing.to_isTopologicalDivisionRing T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
isometry_extensionEmbedding_of_comp 📖	mathematical	Norm.norm NormedField.toNorm DFunLike.coe RingHom WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semiring.toNonAssocSemiring WithAbs.instSemiring NormedField.toField RingHom.instFunLike AbsoluteValue AbsoluteValue.funLike	Isometry UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace UniformSpace.Completion.instMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toMetricSpace Ring.toSemiring UniformSpace.Completion.ring WithAbs.instRing DivisionRing.toRing Field.toDivisionRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing UniformSpace.toTopologicalSpace NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup NormedRing.toRing NormedCommRing.toNormedRing Isometry.extensionHom CompletableTopField.toT0Space completableTopField_of_complete T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass	—	Isometry.completion_extension CompletableTopField.toT0Space completableTopField_of_complete NormedDivisionRing.to_isTopologicalDivisionRing T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
locallyCompactSpace 📖	mathematical	Isometry WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace WithAbs.normedField DFunLike.coe RingHom Semiring.toNonAssocSemiring WithAbs.instSemiring NormedField.toField RingHom.instFunLike	LocallyCompactSpace AbsoluteValue.Completion UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	Topology.IsClosedEmbedding.locallyCompactSpace Isometry.isClosedEmbedding UniformSpace.Completion.completeSpace Isometry.completion_extension CompletableTopField.toT0Space completableTopField_of_complete NormedDivisionRing.to_isTopologicalDivisionRing T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity

WithAbs

Definitions

Name	Category	Theorems
instField 📖	CompOp	1 math math: instFiniteDimensional
normedField 📖	CompOp	26 math math: AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs, NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal, NumberField.InfinitePlace.isometry_embedding, NumberField.InfiniteAdeleRing.algebraMap_apply, NumberField.InfinitePlace.Completion.norm_coe, isometry_of_comp, uniformSpace_comap_eq_of_comp, NumberField.InfinitePlace.Completion.isometry_extensionEmbedding, tendsto_one_div_one_add_pow_nhds_one, NumberField.InfinitePlace.Completion.locallyCompactSpace, NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe, NumberField.InfinitePlace.Completion.extensionEmbedding_coe, NumberField.InfinitePlace.denseRange_algebraMap_pi, NumberField.InfinitePlace.isometry_embedding_of_isReal, AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp, AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp, NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal_coe, isUniformInducing_of_comp, pseudoMetricSpace_induced_of_comp, NumberField.AdeleRing.algebraMap_fst_apply, NumberField.InfinitePlace.Completion.isometry_extensionEmbedding_of_isReal, NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv, NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion, AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp, AbsoluteValue.isEquiv_iff_isHomeomorph, AbsoluteValue.Completion.extensionEmbedding_of_comp_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteDimensional 📖	mathematical	—	FiniteDimensional WithAbs DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Field.toDivisionRing instField Ring.toAddCommGroup DivisionRing.toRing instModule_left	—	—
instIsSeparable 📖	mathematical	—	Algebra.IsSeparable WithAbs DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing instAlgebra_left Semifield.toCommSemiring Ring.toSemiring	—	—
isUniformInducing_of_comp 📖	mathematical	Norm.norm NormedField.toNorm DFunLike.coe RingHom WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semiring.toNonAssocSemiring instSemiring NormedField.toField RingHom.instFunLike AbsoluteValue AbsoluteValue.funLike	IsUniformInducing PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing normedField	—	Isometry.isUniformInducing AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
isometry_of_comp 📖	mathematical	Norm.norm NormedField.toNorm DFunLike.coe RingHom WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semiring.toNonAssocSemiring instSemiring NormedField.toField RingHom.instFunLike AbsoluteValue AbsoluteValue.funLike	Isometry EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace normedField	—	AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
pseudoMetricSpace_induced_of_comp 📖	mathematical	Norm.norm NormedField.toNorm DFunLike.coe RingHom WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semiring.toNonAssocSemiring instSemiring NormedField.toField RingHom.instFunLike AbsoluteValue AbsoluteValue.funLike	PseudoMetricSpace.induced PseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace normedField	—	PseudoMetricSpace.ext Dist.ext Isometry.dist_eq AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
tendsto_one_div_one_add_pow_nhds_one 📖	mathematical	Real Real.instLT DFunLike.coe AbsoluteValue DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder AbsoluteValue.funLike Real.instOne	Filter.Tendsto WithAbs RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm equiv DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing normedField instRing	—	one_div map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass map_pow tendsto_inv_iff₀ IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing one_ne_zero NeZero.one instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing tendsto_iff_norm_sub_tendsto_zero inv_one add_sub_cancel_left norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Real.instIsStrictOrderedRing Real.instArchimedean instOrderTopologyReal abs_norm
uniformSpace_comap_eq_of_comp 📖	mathematical	Norm.norm NormedField.toNorm DFunLike.coe RingHom WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semiring.toNonAssocSemiring instSemiring NormedField.toField RingHom.instFunLike AbsoluteValue AbsoluteValue.funLike	UniformSpace.comap UniformSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace normedField	—	IsUniformInducing.comap_uniformSpace Isometry.isUniformInducing AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass

---

← Back to Index