Padic

📁 Source: FLT/HaarMeasure/HaarChar/Padic.lean

Statistics

Metric	Count
Definitions	0
Theorems ringHaarChar_padic, ringHaarChar_padicInt, volume_padicInt_smul, volume_padic_smul, volume_padicInt_smul	5
Total	5

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringHaarChar_padic 📖	mathematical	—	ringHaarChar Padic.instMeasurableSpace Padic.instBorelSpace	—	Padic.instBorelSpace PadicInt.closure_nonZeroDivisors_padicInt
ringHaarChar_padicInt 📖	mathematical	—	ringHaarChar PadicInt.instMeasurableSpace PadicInt.instBorelSpace	—	ringHaarChar_eq_of_measure_smul_eq_mul PadicInt.instBorelSpace PadicInt.instIsAddHaarMeasure PadicInt.volume_univ PadicInt.instIsFiniteMeasure

Padic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
volume_padicInt_smul 📖	mathematical	—	instMeasureSpace	—	volume_padic_smul
volume_padic_smul 📖	mathematical	—	instMeasureSpace	—	instBorelSpace instIsAddHaarMeasure MeasureTheory.ringHaarChar_padic MeasureTheory.ringHaarChar_mul_volume

PadicInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
volume_padicInt_smul 📖	mathematical	—	instMeasureSpace	—	volume_coe Padic.volume_padicInt_smul

---

← Back to Index