InfiniteAdeleRing

📁 Source: Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean

Statistics

Metric	Count
Definitions InfiniteAdeleRing, instAlgebra, instCommRing, instInhabited, instTopologicalSpace, ringEquiv_mixedSpace	6
Theorems algebraMap_apply, denseRange_algebraMap, instIsTopologicalRing, instNontrivial, locallyCompactSpace, mixedEmbedding_eq_algebraMap_comp, ringEquiv_mixedSpace_apply	7
Total	13

NumberField

Definitions

Name	Category	Theorems
InfiniteAdeleRing 📖	CompOp	9 math math: InfiniteAdeleRing.algebraMap_apply, InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, AdeleRing.algebraMap_snd_apply, InfiniteAdeleRing.instIsTopologicalRing, InfiniteAdeleRing.locallyCompactSpace, AdeleRing.algebraMap_fst_apply, InfiniteAdeleRing.instNontrivial, InfiniteAdeleRing.denseRange_algebraMap, InfiniteAdeleRing.ringEquiv_mixedSpace_apply

NumberField.InfiniteAdeleRing

Definitions

Name	Category	Theorems
instAlgebra 📖	CompOp	3 math math: algebraMap_apply, mixedEmbedding_eq_algebraMap_comp, denseRange_algebraMap
instCommRing 📖	CompOp	5 math math: algebraMap_apply, mixedEmbedding_eq_algebraMap_comp, instIsTopologicalRing, denseRange_algebraMap, ringEquiv_mixedSpace_apply
instInhabited 📖	CompOp	—
instTopologicalSpace 📖	CompOp	3 math math: instIsTopologicalRing, locallyCompactSpace, denseRange_algebraMap
ringEquiv_mixedSpace 📖	CompOp	2 math math: mixedEmbedding_eq_algebraMap_comp, ringEquiv_mixedSpace_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom NumberField.InfiniteAdeleRing Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield CommRing.toCommSemiring instCommRing RingHom.instFunLike algebraMap instAlgebra UniformSpace.Completion.coe' WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring AbsoluteValue Complex Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField	—	—
denseRange_algebraMap 📖	mathematical	—	DenseRange NumberField.InfiniteAdeleRing instTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield CommRing.toCommSemiring instCommRing RingHom.instFunLike algebraMap instAlgebra	—	DenseRange.comp Complex.instNontrivial DenseRange.piMap UniformSpace.Completion.denseRange_coe NumberField.InfinitePlace.denseRange_algebraMap_pi Continuous.piMap UniformSpace.Completion.continuous_coe
instIsTopologicalRing 📖	mathematical	—	IsTopologicalRing NumberField.InfiniteAdeleRing instTopologicalSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing	—	Pi.instIsTopologicalRing Complex.instNontrivial UniformSpace.Completion.topologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup
instNontrivial 📖	mathematical	—	Nontrivial NumberField.InfiniteAdeleRing	—	NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed Pi.nontrivial_at Complex.instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing
locallyCompactSpace 📖	mathematical	—	LocallyCompactSpace NumberField.InfiniteAdeleRing instTopologicalSpace	—	Pi.locallyCompactSpace_of_finite Complex.instNontrivial NumberField.InfinitePlace.Completion.locallyCompactSpace Finite.of_fintype
mixedEmbedding_eq_algebraMap_comp 📖	mathematical	—	DFunLike.coe RingHom NumberField.mixedEmbedding.mixedSpace Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding RingEquiv NumberField.InfiniteAdeleRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Prod.instMul Pi.instMul Real.instMul Complex.instMul Distrib.toAdd Prod.instAdd Pi.instAdd Real.instAdd Complex.instAdd EquivLike.toFunLike RingEquiv.instEquivLike ringEquiv_mixedSpace CommSemiring.toSemiring Semifield.toCommSemiring CommRing.toCommSemiring algebraMap instAlgebra	—	Subtype.prop NumberField.mixedEmbedding.mixedEmbedding_apply_isReal Complex.instNontrivial NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe NumberField.InfinitePlace.Completion.extensionEmbedding_coe NumberField.mixedEmbedding.mixedEmbedding_apply_isComplex
ringEquiv_mixedSpace_apply 📖	mathematical	—	DFunLike.coe RingEquiv NumberField.InfiniteAdeleRing NumberField.mixedEmbedding.mixedSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Prod.instMul Pi.instMul NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instMul NumberField.InfinitePlace.IsComplex Complex Complex.instMul Distrib.toAdd Prod.instAdd Pi.instAdd Real.instAdd Complex.instAdd EquivLike.toFunLike RingEquiv.instEquivLike ringEquiv_mixedSpace RingHom NumberField.InfinitePlace.Completion Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NumberField.InfinitePlace.Completion.instNormedField Real.semiring RingHom.instFunLike NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal Complex.instSemiring NumberField.InfinitePlace.Completion.extensionEmbedding	—	—

---

← Back to Index