Teichmuller

📁 Source: ClassFieldTheory/LocalCFT/Teichmuller.lean

Statistics

Metric	Count
Definitions `teichmuller`, `teichmuller'`, `teichmullerSeq`	3
Theorems `cauchySeq_iff`, `cauchySeq_iff'`, `cauchySeq_of_succ`, `cauchySeq_teichmuller`, `ext_maximalIdeal`, `ext_maximalIdeal'`, `hasBasis_nhds`, `hasBasis_nhds_integer`, `hasBasis_uniformity`, `isClosed_closedBall'`, `leftInverse_teichmuller'`, `limUnder_teichmullerSeq_mem`, `map_irreducible`, `mem_maximalIdeal_pow_iff`, `pow_card_sub_mem`, `pow_sub_pow_mem`, `residue_comp_teichmuller'`, `residue_teichmuller'`, `teichmuller'_def`, `teichmuller'_injective`, `teichmullerSeq_add_sub_mem`, `teichmullerSeq_apply`, `teichmullerSeq_sub_teichmullerSeq_mem`, `teichmullerSeq_succ_sub_mem`, `teichmuller_def`, `teichmuller_eq_teichmuller'`, `teichmuller_injective`	27
Total	30

IsNonarchimedeanLocalField

Definitions

Name	Category	Theorems
`teichmuller` 📖	CompOp	3 math math: `teichmuller_eq_teichmuller'`, `teichmuller_def`, `teichmuller_injective`
`teichmuller'` 📖	CompOp	6 math math: `teichmuller'_injective`, `leftInverse_teichmuller'`, `teichmuller_eq_teichmuller'`, `residue_comp_teichmuller'`, `residue_teichmuller'`, `teichmuller'_def`
`teichmullerSeq` 📖	CompOp	8 math math: `teichmullerSeq_add_sub_mem`, `limUnder_teichmullerSeq_mem`, `teichmullerSeq_sub_teichmullerSeq_mem`, `teichmullerSeq_succ_sub_mem`, `cauchySeq_teichmuller`, `teichmuller_def`, `teichmullerSeq_apply`, `teichmuller'_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchySeq_iff` 📖	—	—	—	—	`cauchySeq_iff'`
`cauchySeq_iff'` 📖	—	—	—	—	`hasBasis_uniformity`
`cauchySeq_of_succ` 📖	—	—	—	—	`cauchySeq_iff'`
`cauchySeq_teichmuller` 📖	mathematical	—	`teichmullerSeq`	—	`cauchySeq_of_succ` `teichmullerSeq_succ_sub_mem`
`ext_maximalIdeal` 📖	—	—	—	—	—
`ext_maximalIdeal'` 📖	—	—	—	—	`ext_maximalIdeal`
`hasBasis_nhds` 📖	—	—	—	—	`Filter.HasBasis.comp_dense'` `OrderMonoidIso.surjective`
`hasBasis_nhds_integer` 📖	—	—	—	—	`mem_maximalIdeal_pow_iff` `OrderMonoidIso.lt_symm_apply` `WithZero.lt_exp_iff` `OrderMonoidIso.le_symm_apply` `hasBasis_nhds`
`hasBasis_uniformity` 📖	—	—	—	—	`IsUniformAddGroup.addSubgroupClass` `hasBasis_nhds_integer`
`isClosed_closedBall'` 📖	—	—	—	—	—
`leftInverse_teichmuller'` 📖	mathematical	—	`teichmuller'`	—	`residue_teichmuller'`
`limUnder_teichmullerSeq_mem` 📖	mathematical	—	`teichmullerSeq`	—	`isClosed_closedBall'` `teichmullerSeq_add_sub_mem` `cauchySeq_teichmuller`
`map_irreducible` 📖	—	—	—	—	`valueGroupWithZeroIsoInt_irreducible`
`mem_maximalIdeal_pow_iff` 📖	—	—	—	—	`Valuation.algebraMap_integer_coe` `map_irreducible`
`pow_card_sub_mem` 📖	—	—	—	—	`FiniteField.pow_natCard`
`pow_sub_pow_mem` 📖	—	—	—	—	—
`residue_comp_teichmuller'` 📖	mathematical	—	`teichmuller'`	—	`residue_teichmuller'`
`residue_teichmuller'` 📖	mathematical	—	`teichmuller'`	—	`limUnder_teichmullerSeq_mem`
`teichmuller'_def` 📖	mathematical	—	`teichmullerSeq` `teichmuller'`	—	`cauchySeq_teichmuller`
`teichmuller'_injective` 📖	mathematical	—	`teichmuller'`	—	`leftInverse_teichmuller'`
`teichmullerSeq_add_sub_mem` 📖	mathematical	—	`teichmullerSeq`	—	`teichmullerSeq_succ_sub_mem`
`teichmullerSeq_apply` 📖	mathematical	—	`teichmullerSeq`	—	—
`teichmullerSeq_sub_teichmullerSeq_mem` 📖	mathematical	—	`teichmullerSeq`	—	`pow_sub_pow_mem`
`teichmullerSeq_succ_sub_mem` 📖	mathematical	—	`teichmullerSeq`	—	`pow_card_sub_mem` `pow_sub_pow_mem`
`teichmuller_def` 📖	mathematical	—	`teichmullerSeq` `teichmuller`	—	`teichmuller'_def`
`teichmuller_eq_teichmuller'` 📖	mathematical	—	`teichmuller` `teichmuller'`	—	—
`teichmuller_injective` 📖	mathematical	—	`teichmuller`	—	`teichmuller'_injective`

---

← Back to Index