InfiniteAdeleRing

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

Statistics

Metric	Count
Definitions algEquiv_mixedSpace, continuousAlgEquiv_mixedSpace, infinitePlace_completion_continuousAlgEquiv, instAlgebraRealInfiniteAdeleRing_fLT	4
Theorems infinitePlace_completion_continuousAlgEquiv_apply_algebraMap, instFiniteRealInfiniteAdeleRing_fLT, instIsModuleTopologyRealComplex_fLT, instIsModuleTopologyRealInfiniteAdeleRing_fLT, instSecondCountableTopologyInfiniteAdeleRing_fLT, instT2SpaceInfiniteAdeleRing_fLT	6
Total	10

NumberField.InfiniteAdeleRing

Definitions

Name	Category	Theorems
algEquiv_mixedSpace 📖	CompOp	—
continuousAlgEquiv_mixedSpace 📖	CompOp	—

Rat

Definitions

Name	Category	Theorems
infinitePlace_completion_continuousAlgEquiv 📖	CompOp	1 math math: infinitePlace_completion_continuousAlgEquiv_apply_algebraMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infinitePlace_completion_continuousAlgEquiv_apply_algebraMap 📖	mathematical	—	infinitePlace_completion_continuousAlgEquiv	—	—

(root)

Definitions

Name	Category	Theorems
instAlgebraRealInfiniteAdeleRing_fLT 📖	CompOp	4 math math: NumberField.AdeleRing.DivisionAlgebra.Aux.instIsScalarTowerRealInfiniteAdeleRingDinf, instIsModuleTopologyRealInfiniteAdeleRing_fLT, NumberField.InfiniteAdeleRing.algebraMap_completion, instFiniteRealInfiniteAdeleRing_fLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteRealInfiniteAdeleRing_fLT 📖	mathematical	—	instAlgebraRealInfiniteAdeleRing_fLT	—	—
instIsModuleTopologyRealComplex_fLT 📖	—	—	—	—	—
instIsModuleTopologyRealInfiniteAdeleRing_fLT 📖	mathematical	—	instAlgebraRealInfiniteAdeleRing_fLT	—	instIsModuleTopologyRealComplex_fLT
instSecondCountableTopologyInfiniteAdeleRing_fLT 📖	—	—	—	—	instSecondCountableTopologyCompletion_fLT
instT2SpaceInfiniteAdeleRing_fLT 📖	—	—	—	—	—

---

← Back to Index