Completion

📁 Source: Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean

Statistics

Metric	Count
Definitions Completion, extensionEmbedding, extensionEmbeddingOfIsReal, instAlgebra, instNormedField, isometryEquivComplexOfIsComplex, isometryEquivRealOfIsReal, ringEquivComplexOfIsComplex, ringEquivRealOfIsReal	9
Theorems norm_infinitePlace_completion, ratCast_equiv, bijective_extensionEmbeddingOfIsReal, bijective_extensionEmbedding_of_isComplex, bijective_extensionEmbedding_of_isReal, extensionEmbeddingOfIsReal_coe, extensionEmbedding_coe, extensionEmbedding_of_isReal_coe, isClosed_image_extensionEmbedding, isClosed_image_extensionEmbeddingOfIsReal, isClosed_image_extensionEmbedding_of_isReal, isometry_extensionEmbedding, isometry_extensionEmbeddingOfIsReal, isometry_extensionEmbedding_of_isReal, locallyCompactSpace, norm_coe, subfield_ne_real_of_isComplex, surjective_extensionEmbeddingOfIsReal, surjective_extensionEmbedding_of_isComplex, surjective_extensionEmbedding_of_isReal, isometry_embedding, isometry_embedding_of_isReal	22
Total	31

NumberField.InfinitePlace

Definitions

Name	Category	Theorems
Completion 📖	CompOp	18 math math: Completion.isometry_extensionEmbeddingOfIsReal, Completion.surjective_extensionEmbedding_of_isComplex, Completion.isometry_extensionEmbedding, Completion.locallyCompactSpace, Completion.isClosed_image_extensionEmbedding, Completion.extensionEmbeddingOfIsReal_coe, Completion.bijective_extensionEmbedding_of_isReal, Completion.isClosed_image_extensionEmbeddingOfIsReal, Completion.isClosed_image_extensionEmbedding_of_isReal, Completion.extensionEmbedding_coe, Completion.bijective_extensionEmbeddingOfIsReal, Completion.bijective_extensionEmbedding_of_isComplex, Completion.extensionEmbedding_of_isReal_coe, Completion.surjective_extensionEmbedding_of_isReal, Completion.surjective_extensionEmbeddingOfIsReal, Completion.isometry_extensionEmbedding_of_isReal, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, Completion.Rat.norm_infinitePlace_completion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isometry_embedding 📖	mathematical	—	Isometry WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace WithAbs.normedField DFunLike.coe WithAbs.instSemiring RingHom.instFunLike RingHom.comp embedding RingEquiv.toRingHom WithAbs.equiv	—	AddMonoidHomClass.isometry_of_norm Complex.instNontrivial RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass norm_embedding_eq
isometry_embedding_of_isReal 📖	mathematical	IsReal	Isometry WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace WithAbs.normedField Real.metricSpace DFunLike.coe WithAbs.instSemiring RingHom.instFunLike RingHom.comp embedding_of_isReal RingEquiv.toRingHom WithAbs.equiv	—	AddMonoidHomClass.isometry_of_norm Complex.instNontrivial RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass norm_embedding_of_isReal

NumberField.InfinitePlace.Completion

Definitions

Name	Category	Theorems
extensionEmbedding 📖	CompOp	6 math math: surjective_extensionEmbedding_of_isComplex, isometry_extensionEmbedding, isClosed_image_extensionEmbedding, extensionEmbedding_coe, bijective_extensionEmbedding_of_isComplex, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply
extensionEmbeddingOfIsReal 📖	CompOp	11 math math: isometry_extensionEmbeddingOfIsReal, extensionEmbeddingOfIsReal_coe, bijective_extensionEmbedding_of_isReal, isClosed_image_extensionEmbeddingOfIsReal, isClosed_image_extensionEmbedding_of_isReal, bijective_extensionEmbeddingOfIsReal, extensionEmbedding_of_isReal_coe, surjective_extensionEmbedding_of_isReal, surjective_extensionEmbeddingOfIsReal, isometry_extensionEmbedding_of_isReal, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply
instAlgebra 📖	CompOp	—
instNormedField 📖	CompOp	18 math math: isometry_extensionEmbeddingOfIsReal, surjective_extensionEmbedding_of_isComplex, isometry_extensionEmbedding, isClosed_image_extensionEmbedding, extensionEmbeddingOfIsReal_coe, bijective_extensionEmbedding_of_isReal, isClosed_image_extensionEmbeddingOfIsReal, isClosed_image_extensionEmbedding_of_isReal, extensionEmbedding_coe, bijective_extensionEmbeddingOfIsReal, bijective_extensionEmbedding_of_isComplex, extensionEmbedding_of_isReal_coe, surjective_extensionEmbedding_of_isReal, surjective_extensionEmbeddingOfIsReal, isometry_extensionEmbedding_of_isReal, WithAbs.ratCast_equiv, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, Rat.norm_infinitePlace_completion
isometryEquivComplexOfIsComplex 📖	CompOp	—
isometryEquivRealOfIsReal 📖	CompOp	—
ringEquivComplexOfIsComplex 📖	CompOp	—
ringEquivRealOfIsReal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_extensionEmbeddingOfIsReal 📖	mathematical	NumberField.InfinitePlace.IsReal	Function.Bijective NumberField.InfinitePlace.Completion Real DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal	—	RingHom.injective Complex.instNontrivial SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing DivisionRing.isSimpleRing Real.instNontrivial surjective_extensionEmbeddingOfIsReal
bijective_extensionEmbedding_of_isComplex 📖	mathematical	NumberField.InfinitePlace.IsComplex	Function.Bijective NumberField.InfinitePlace.Completion Complex DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Complex.instSemiring RingHom.instFunLike extensionEmbedding	—	RingHom.injective Complex.instNontrivial SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing DivisionRing.isSimpleRing surjective_extensionEmbedding_of_isComplex
bijective_extensionEmbedding_of_isReal 📖	mathematical	NumberField.InfinitePlace.IsReal	Function.Bijective NumberField.InfinitePlace.Completion Real DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal	—	bijective_extensionEmbeddingOfIsReal
extensionEmbeddingOfIsReal_coe 📖	mathematical	NumberField.InfinitePlace.IsReal	DFunLike.coe RingHom NumberField.InfinitePlace.Completion Real Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal UniformSpace.Completion.coe' WithAbs Real.partialOrder AbsoluteValue Complex Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField NumberField.InfinitePlace.embedding_of_isReal	—	Isometry.extensionHom_coe Complex.instNontrivial IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup instIsUniformAddGroupReal instIsTopologicalRingReal Real.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding_of_isReal
extensionEmbedding_coe 📖	mathematical	—	DFunLike.coe RingHom NumberField.InfinitePlace.Completion Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Complex.instSemiring RingHom.instFunLike extensionEmbedding UniformSpace.Completion.coe' WithAbs Real Real.semiring Real.partialOrder AbsoluteValue NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField NumberField.InfinitePlace.embedding	—	Isometry.extensionHom_coe Complex.instNontrivial IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup Complex.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding
extensionEmbedding_of_isReal_coe 📖	mathematical	NumberField.InfinitePlace.IsReal	DFunLike.coe RingHom NumberField.InfinitePlace.Completion Real Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal UniformSpace.Completion.coe' WithAbs Real.partialOrder AbsoluteValue Complex Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField NumberField.InfinitePlace.embedding_of_isReal	—	extensionEmbeddingOfIsReal_coe
isClosed_image_extensionEmbedding 📖	mathematical	—	IsClosed Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set.range NumberField.InfinitePlace.Completion DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Complex.instSemiring RingHom.instFunLike extensionEmbedding	—	Topology.IsClosedEmbedding.isClosed_range Complex.instNontrivial Isometry.isClosedEmbedding UniformSpace.Completion.completeSpace Isometry.completion_extension Complex.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding
isClosed_image_extensionEmbeddingOfIsReal 📖	mathematical	NumberField.InfinitePlace.IsReal	IsClosed Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.range NumberField.InfinitePlace.Completion DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal	—	Topology.IsClosedEmbedding.isClosed_range Complex.instNontrivial Isometry.isClosedEmbedding UniformSpace.Completion.completeSpace Isometry.completion_extension Real.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding_of_isReal
isClosed_image_extensionEmbedding_of_isReal 📖	mathematical	NumberField.InfinitePlace.IsReal	IsClosed Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.range NumberField.InfinitePlace.Completion DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal	—	isClosed_image_extensionEmbeddingOfIsReal
isometry_extensionEmbedding 📖	mathematical	—	Isometry NumberField.InfinitePlace.Completion Complex EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace UniformSpace.Completion.instMetricSpace WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AbsoluteValue RingHom Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField NormedField.toMetricSpace DFunLike.coe NormedField.toField instNormedField RingHom.instFunLike extensionEmbedding	—	Isometry.completion_extension Complex.instNontrivial Complex.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding
isometry_extensionEmbeddingOfIsReal 📖	mathematical	NumberField.InfinitePlace.IsReal	Isometry NumberField.InfinitePlace.Completion Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace UniformSpace.Completion.instMetricSpace WithAbs Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField Real.metricSpace DFunLike.coe NormedField.toField instNormedField RingHom.instFunLike extensionEmbeddingOfIsReal	—	Isometry.completion_extension Complex.instNontrivial Real.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding_of_isReal
isometry_extensionEmbedding_of_isReal 📖	mathematical	NumberField.InfinitePlace.IsReal	Isometry NumberField.InfinitePlace.Completion Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace UniformSpace.Completion.instMetricSpace WithAbs Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField Real.metricSpace DFunLike.coe NormedField.toField instNormedField RingHom.instFunLike extensionEmbeddingOfIsReal	—	isometry_extensionEmbeddingOfIsReal
locallyCompactSpace 📖	mathematical	—	LocallyCompactSpace NumberField.InfinitePlace.Completion UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField	—	AbsoluteValue.Completion.locallyCompactSpace Complex.instNontrivial Complex.instCompleteSpace locallyCompact_of_proper Complex.instProperSpace NumberField.InfinitePlace.isometry_embedding
norm_coe 📖	mathematical	—	Norm.norm UniformSpace.Completion WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField UniformSpace.Completion.instNorm NormedField.toNorm UniformSpace.Completion.coe' DFunLike.coe NumberField.InfinitePlace NumberField.InfinitePlace.instFunLikeReal RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring WithAbs.instSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike WithAbs.equiv	—	Complex.instNontrivial UniformSpace.Completion.norm_coe
subfield_ne_real_of_isComplex 📖	—	NumberField.InfinitePlace.IsComplex	—	—	Mathlib.Tactic.Contrapose.contrapose₃ RingHom.ext Complex.instNontrivial RingHom.mem_fieldRange_self extensionEmbedding_coe Complex.conj_ofReal
surjective_extensionEmbeddingOfIsReal 📖	mathematical	NumberField.InfinitePlace.IsReal	NumberField.InfinitePlace.Completion Real DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal	—	RingHom.fieldRange_eq_top_iff Real.subfield_eq_of_closed isClosed_image_extensionEmbeddingOfIsReal
surjective_extensionEmbedding_of_isComplex 📖	mathematical	NumberField.InfinitePlace.IsComplex	NumberField.InfinitePlace.Completion Complex DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Complex.instSemiring RingHom.instFunLike extensionEmbedding	—	RingHom.fieldRange_eq_top_iff Complex.subfield_eq_of_closed isClosed_image_extensionEmbedding subfield_ne_real_of_isComplex
surjective_extensionEmbedding_of_isReal 📖	mathematical	NumberField.InfinitePlace.IsReal	NumberField.InfinitePlace.Completion Real DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal	—	surjective_extensionEmbeddingOfIsReal

NumberField.InfinitePlace.Completion.Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_infinitePlace_completion 📖	mathematical	—	Norm.norm NumberField.InfinitePlace.Completion Rat.instField UniformSpace.Completion.instNorm WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField NormedField.toNorm DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NumberField.InfinitePlace.Completion.instNormedField Real.instRatCast abs Rat.instLattice Rat.addGroup	—	Complex.instNontrivial RingEquiv.apply_symm_apply NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv NumberField.InfinitePlace.Completion.norm_coe Rat.infinitePlace_apply

NumberField.InfinitePlace.Completion.WithAbs

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ratCast_equiv 📖	mathematical	—	UniformSpace.Completion WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Rat.instField AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NumberField.InfinitePlace.Completion.instNormedField DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring WithAbs.instSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike WithAbs.equiv UniformSpace.Completion.coe'	—	Complex.instNontrivial eq_ratCast RingHom.instRingHomClass

---

← Back to Index