Documentation Verification Report

InfiniteAdeleRing

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

Statistics

Metric	Count
Definitions `InfiniteAdeleRing`, `instAlgebra`, `instCommRing`, `instInhabited`, `instNorm`, `instTopologicalSpace`, `ringEquiv_mixedSpace`	7
Theorems `algebraMap_apply`, `coe_norm_eq_abs_norm`, `denseRange_algebraMap`, `instIsTopologicalRing`, `instNontrivial`, `locallyCompactSpace`, `mixedEmbedding_eq_algebraMap_comp`, `norm_def`, `norm_eq_zero_of_not_isUnit`, `ringEquiv_mixedSpace_apply`	10
Total	17

NumberField

Definitions

Name	Category	Theorems
`InfiniteAdeleRing` 📖	CompOp	12 math math: `InfiniteAdeleRing.algebraMap_apply`, `InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp`, `AdeleRing.algebraMap_snd_apply`, `InfiniteAdeleRing.instIsTopologicalRing`, `InfiniteAdeleRing.norm_eq_zero_of_not_isUnit`, `InfiniteAdeleRing.locallyCompactSpace`, `AdeleRing.algebraMap_fst_apply`, `InfiniteAdeleRing.coe_norm_eq_abs_norm`, `InfiniteAdeleRing.norm_def`, `InfiniteAdeleRing.instNontrivial`, `InfiniteAdeleRing.denseRange_algebraMap`, `InfiniteAdeleRing.ringEquiv_mixedSpace_apply`

NumberField.InfiniteAdeleRing

Definitions

Name	Category	Theorems
`instAlgebra` 📖	CompOp	4 math math: `algebraMap_apply`, `mixedEmbedding_eq_algebraMap_comp`, `coe_norm_eq_abs_norm`, `denseRange_algebraMap`
`instCommRing` 📖	CompOp	6 math math: `algebraMap_apply`, `mixedEmbedding_eq_algebraMap_comp`, `instIsTopologicalRing`, `coe_norm_eq_abs_norm`, `denseRange_algebraMap`, `ringEquiv_mixedSpace_apply`
`instInhabited` 📖	CompOp	—
`instNorm` 📖	CompOp	3 math math: `norm_eq_zero_of_not_isUnit`, `coe_norm_eq_abs_norm`, `norm_def`
`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` `WithAbs.toAbs`	—	—
`coe_norm_eq_abs_norm` 📖	mathematical	—	`Norm.norm` `NumberField.InfiniteAdeleRing` `instNorm` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Real` `Real.instRatCast` `abs` `Rat.instLattice` `Rat.addGroup` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `Rat.commRing` `MonoidHom.instFunLike` `Algebra.norm` `DivisionRing.toRatAlgebra` `NumberField.to_charZero`	—	`NumberField.to_charZero` `Complex.instNontrivial` `Finset.prod_congr` `UniformSpace.Completion.norm_coe` `NumberField.InfinitePlace.prod_eq_abs_norm`
`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` `NumberField.InfinitePlace.Completion.instIsTopologicalRing`
`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`
`norm_def` 📖	mathematical	—	`Norm.norm` `NumberField.InfiniteAdeleRing` `instNorm` `Finset.prod` `NumberField.InfinitePlace` `Real` `Real.instCommMonoid` `Finset.univ` `NumberField.InfinitePlace.NumberField.InfinitePlace.fintype` `Monoid.toPow` `Real.instMonoid` `NumberField.InfinitePlace.Completion` `UniformSpace.Completion.instNorm` `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` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `WithAbs.normedField` `NormedField.toNorm` `NumberField.InfinitePlace.mult`	—	—
`norm_eq_zero_of_not_isUnit` 📖	mathematical	`IsUnit` `NumberField.InfiniteAdeleRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	`Norm.norm` `NumberField.InfiniteAdeleRing` `instNorm` `Real` `Real.instZero`	—	`Pi.isUnit_iff` `Complex.instNontrivial` `Finset.prod_eq_zero_iff` `Real.instNontrivial` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Finset.mem_univ` `isReduced_of_noZeroDivisors`
`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