InfinitePlace

📁 Source: FLT/Mathlib/MeasureTheory/Constructions/BorelSpace/InfinitePlace.lean

Statistics

Metric	Count
Definitions instMeasurableSpaceCompletion_fLT, instMeasurableSpaceInfiniteAdeleRing_fLT	2
Theorems instBorelSpaceCompletion_fLT, instBorelSpaceInfiniteAdeleRing_fLT	2
Total	4

(root)

Definitions

Name	Category	Theorems
instMeasurableSpaceCompletion_fLT 📖	CompOp	2 math math: Rat.AdeleRing.isAddFundamentalDomain, instBorelSpaceCompletion_fLT
instMeasurableSpaceInfiniteAdeleRing_fLT 📖	CompOp	2 math math: instBorelSpaceInfiniteAdeleRing_fLT, MeasureTheory.ringHaarChar_adeles_rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instBorelSpaceCompletion_fLT 📖	mathematical	—	instMeasurableSpaceCompletion_fLT	—	—
instBorelSpaceInfiniteAdeleRing_fLT 📖	mathematical	—	instMeasurableSpaceInfiniteAdeleRing_fLT	—	instSecondCountableTopologyCompletion_fLT instBorelSpaceCompletion_fLT

---

← Back to Index