Continuity

📁 Source: ClassFieldTheory/LocalCFT/Continuity.lean

Statistics

Metric	Count
Definitions	0
Theorems sum_eq_iSup, continuous_algebraMap_of_density, exists_valuation_algebraMap_eq_valuation_pow, exists_valuation_algebraMap_le_valuation, instContinuousSMul_classFieldTheory	5
Total	5

Valuation

Theorems

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

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_algebraMap_of_density 📖	—	—	—	—	ValuativeRel.unitsMap_valuation_surjective exists_valuation_algebraMap_le_valuation ValuativeExtension.algebraMap_lt
exists_valuation_algebraMap_eq_valuation_pow 📖	—	—	—	—	Valuation.sum_eq_iSup
exists_valuation_algebraMap_le_valuation 📖	—	—	—	—	exists_valuation_algebraMap_eq_valuation_pow
instContinuousSMul_classFieldTheory 📖	—	—	—	—	continuous_algebraMap_of_density

---

← Back to Index