Finite

📁 Source: FLT/NumberField/Completion/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems instCompactSpaceAdicCompletionIntegers, instFiniteResidueFieldAdicCompletionIntegers, isCompactAdicCompletionIntegers, isOpenAdicCompletionIntegers, locallyCompactSpace, instFiniteResidueFieldAdicCompletionRingOfIntegersWithZeroMultiplicativeInt_fLT, instLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT, instWeaklyLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT	8
Total	8

NumberField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompactSpaceAdicCompletionIntegers 📖	—	—	—	—	Valued.WithZeroMulInt.integer_compactSpace IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeInt_fLT instFiniteResidueFieldAdicCompletionRingOfIntegersWithZeroMultiplicativeInt_fLT
instFiniteResidueFieldAdicCompletionIntegers 📖	—	—	—	—	—
isCompactAdicCompletionIntegers 📖	—	—	—	—	instCompactSpaceAdicCompletionIntegers
isOpenAdicCompletionIntegers 📖	—	—	—	—	—

Rat.adicCompletion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	—	—	—	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteResidueFieldAdicCompletionRingOfIntegersWithZeroMultiplicativeInt_fLT 📖	—	—	—	—	NumberField.instFiniteResidueFieldAdicCompletionIntegers
instLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT 📖	—	—	—	—	instWeaklyLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT
instWeaklyLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT 📖	—	—	—	—	NumberField.instCompactSpaceAdicCompletionIntegers NumberField.isOpenAdicCompletionIntegers

---

← Back to Index