FiniteAdeleRing

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

Statistics

Metric	Count
Definitions	0
Theorems instCompactSpaceSubtypeFiniteAdeleRingRingOfIntegersMemSubringIntegralAdeles, instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT, instSecondCountableTopologyFiniteAdeleRingRingOfIntegers_fLT, instT2SpaceFiniteAdeleRingRingOfIntegers_fLT	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompactSpaceSubtypeFiniteAdeleRingRingOfIntegersMemSubringIntegralAdeles 📖	mathematical	—	IsDedekindDomain.FiniteAdeleRing.integralAdeles	—	NumberField.instCompactSpaceAdicCompletionIntegers
instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT 📖	—	—	—	—	NumberField.isOpenAdicCompletionIntegers NumberField.instCompactSpaceAdicCompletionIntegers
instSecondCountableTopologyFiniteAdeleRingRingOfIntegers_fLT 📖	—	—	—	—	RestrictedProduct.secondCountableTopology instCountableHeightOneSpectrumRingOfIntegers_fLT NumberField.isOpenAdicCompletionIntegers IsDedekindDomain.HeightOneSpectrum.instSeparableSpaceAdicCompletionOfCountable_fLT instCountableOfNumberField_fLT
instT2SpaceFiniteAdeleRingRingOfIntegers_fLT 📖	—	—	—	—	—

---

← Back to Index