Structures · Topology
NonarchimedeanGroup
A topological group is nonarchimedean if every neighborhood of 1 contains an open subgroup.
- Shape
- One type argument · adds is_nonarchimedean
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- NonarchimedeanGroup.is_nonarchimedean
- NonarchimedeanGroup.cauchySeq_prod_of_tendsto_cofinite_one
- NonarchimedeanGroup.multipliable_of_tendsto_cofinite_one
- NonarchimedeanGroup.prod_subset
- NonarchimedeanGroup.exists_openSubgroup_separating
- NonarchimedeanGroup.Prod.instNonarchimedeanGroup
- NonarchimedeanGroup.instTotallySeparated
- NonarchimedeanGroup.prod_self_subset
- NonarchimedeanGroup.nonarchimedean_of_emb
- NonarchimedeanGroup.multipliable_iff_tendsto_cofinite_one
- NonarchimedeanGroup.toIsTopologicalGroup
- NonarchimedeanGroup.cauchySeq_of_tendsto_div_nhds_one