Documentation Verification Report

AdeleRing

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

Statistics

Metric	Count
Definitions `AdeleRing`, `instAlgebra`, `instCommRing`, `instInhabited`, `instTopologicalSpace`, `principalSubgroup`	6
Theorems `algebraMap_fst_apply`, `algebraMap_injective`, `algebraMap_snd_apply`, `instIsTopologicalRing`	4
Total	10

NumberField

Definitions

Name	Category	Theorems
`AdeleRing` 📖	CompOp	4 math math: `AdeleRing.algebraMap_snd_apply`, `AdeleRing.algebraMap_injective`, `AdeleRing.instIsTopologicalRing`, `AdeleRing.algebraMap_fst_apply`

NumberField.AdeleRing

Definitions

Name	Category	Theorems
`instAlgebra` 📖	CompOp	3 math math: `algebraMap_snd_apply`, `algebraMap_injective`, `algebraMap_fst_apply`
`instCommRing` 📖	CompOp	4 math math: `algebraMap_snd_apply`, `algebraMap_injective`, `instIsTopologicalRing`, `algebraMap_fst_apply`
`instInhabited` 📖	CompOp	—
`instTopologicalSpace` 📖	CompOp	1 math math: `instIsTopologicalRing`
`principalSubgroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_fst_apply` 📖	mathematical	—	`NumberField.InfiniteAdeleRing` `IsDedekindDomain.FiniteAdeleRing` `DFunLike.coe` `RingHom` `NumberField.AdeleRing` `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`	—	—
`algebraMap_injective` 📖	mathematical	—	`NumberField.AdeleRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `algebraMap` `instAlgebra`	—	`RingHom.injective` `DivisionRing.isSimpleRing` `NumberField.InfiniteAdeleRing.instNontrivial`
`algebraMap_snd_apply` 📖	mathematical	—	`DFunLike.coe` `IsDedekindDomain.FiniteAdeleRing` `IsDedekindDomain.HeightOneSpectrum` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `IsDedekindDomain.FiniteAdeleRing.instDFunLikeHeightOneSpectrumAdicCompletion` `NumberField.InfiniteAdeleRing` `RingHom` `NumberField.AdeleRing` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `algebraMap` `instAlgebra` `UniformSpace.Completion.coe'` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued`	—	—
`instIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `NumberField.AdeleRing` `instTopologicalSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing`	—	`instIsTopologicalRingProd` `NumberField.InfiniteAdeleRing.instIsTopologicalRing` `IsDedekindDomain.FiniteAdeleRing.instIsTopologicalRing`

---

← Back to Index