Structures · Topology
NonarchimedeanAddGroup
A topological additive group is nonarchimedean if every neighborhood of 0 contains an open subgroup.
- Shape
- One type argument · adds is_nonarchimedean
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- UniformSpace.Completion
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- NonarchimedeanAddGroup.is_nonarchimedean
- NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero
- NonarchimedeanAddGroup.cauchySeq_sum_of_tendsto_cofinite_zero
- NonarchimedeanAddGroup.prod_subset
- NonarchimedeanAddGroup.prod_self_subset
- NonarchimedeanAddGroup.toIsTopologicalAddGroup
- NonarchimedeanAddGroup.cauchySeq_of_tendsto_sub_nhds_zero
- instNonarchimedeanAddGroupCompletion
- NonarchimedeanAddGroup.instTotallySeparated
- NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero
- NonarchimedeanAddGroup.exists_openAddSubgroup_separating
- NonarchimedeanAddGroup.nonarchimedean_of_emb
- NonarchimedeanAddGroup.Prod.instNonarchimedeanAddGroup