Completion

Statistics

Metric	Count
Definitions	0
Theorems `instNonarchimedeanAddGroupCompletion`, `instNonarchimedeanRingCompletion`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonarchimedeanAddGroupCompletion` 📖	mathematical	—	`NonarchimedeanAddGroup` `UniformSpace.Completion` `UniformSpace.Completion.addGroup` `UniformSpace.toTopologicalSpace` `UniformSpace.Completion.uniformSpace`	—	`IsUniformAddGroup.to_topologicalAddGroup` `UniformSpace.Completion.isUniformAddGroup` `Filter.HasBasis.mem_iff` `closed_nhds_basis` `UniformSpace.to_regularSpace` `ContinuousAt.preimage_mem_nhds` `Continuous.continuousAt` `UniformSpace.Completion.continuous_toCompl` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `NonarchimedeanAddGroup.is_nonarchimedean` `AddSubgroup.isOpen_of_mem_nhds` `IsTopologicalAddGroup.toContinuousAdd` `IsDenseInducing.closure_image_mem_nhds` `UniformSpace.Completion.isDenseInducing_toCompl` `OpenAddSubgroup.mem_nhds_zero` `closure_minimal` `Set.image_subset_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset`
`instNonarchimedeanRingCompletion` 📖	mathematical	—	`NonarchimedeanRing` `UniformSpace.Completion` `UniformSpace.Completion.ring` `UniformSpace.toTopologicalSpace` `UniformSpace.Completion.uniformSpace`	—	`UniformSpace.Completion.topologicalRing` `NonarchimedeanAddGroup.is_nonarchimedean` `instNonarchimedeanAddGroupCompletion` `NonarchimedeanRing.to_nonarchimedeanAddGroup`

---