Documentation Verification Report

Nonarchimedean

📁 Source: Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean

Statistics

Metric	Count
Definitions	0
Theorems `mul_of_nonarchimedean`, `cauchySeq_of_tendsto_sub_nhds_zero`, `cauchySeq_sum_of_tendsto_cofinite_zero`, `summable_iff_tendsto_cofinite_zero`, `summable_of_tendsto_cofinite_zero`, `cauchySeq_of_tendsto_div_nhds_one`, `cauchySeq_prod_of_tendsto_cofinite_one`, `multipliable_iff_tendsto_cofinite_one`, `multipliable_of_tendsto_cofinite_one`, `mul_of_nonarchimedean`, `tsum_mul_tsum_of_nonarchimedean`	11
Total	11

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_of_nonarchimedean` 📖	mathematical	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`hasSum_iff_hasSum_compl` `UniformSpace.Completion.coe_mul` `NonarchimedeanRing.toIsTopologicalRing` `mul` `instT3Space` `UniformSpace.Completion.t0Space` `IsTopologicalAddGroup.regularSpace` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `instNonarchimedeanAddGroupCompletion` `NonarchimedeanRing.to_nonarchimedeanAddGroup` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.Completion.topologicalRing` `UniformSpace.Completion.isUniformAddGroup` `instNonarchimedeanRingCompletion` `UniformSpace.Completion.completeSpace` `summable`

NonarchimedeanAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchySeq_of_tendsto_sub_nhds_zero` 📖	mathematical	`Filter.Tendsto` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`CauchySeq`	—	`Filter.tendsto_atTop'` `SemilatticeSup.instIsDirectedOrder` `is_nonarchimedean` `Filter.mem_atTop_sets` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Set.mem_preimage` `SetLike.mem_coe` `Filter.tendsto_def` `OpenAddSubgroup.mem_nhds_zero` `add_zero` `sub_self` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `OpenAddSubgroup.instAddSubgroupClass` `sub_add_sub_cancel` `OpenAddSubgroup.mem_toAddSubgroup` `AddSubgroup.add_mem` `neg_sub` `AddSubgroup.neg_mem` `le_of_not_ge` `cauchy_map_iff` `Filter.atTop_neBot` `Filter.prod_atTop_atTop_eq` `uniformity_eq_comap_nhds_zero` `IsUniformAddGroup.isRightUniformAddGroup` `Filter.tendsto_comap_iff`
`cauchySeq_sum_of_tendsto_cofinite_zero` 📖	mathematical	`Filter.Tendsto` `Filter.cofinite` `nhds` `UniformSpace.toTopologicalSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`CauchySeq` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`cauchySeq_finset_iff_sum_vanishing` `is_nonarchimedean` `Filter.tendsto_def` `OpenAddSubgroup.mem_nhds_zero` `AddSubgroup.sum_mem` `OpenAddSubgroup.mem_toAddSubgroup` `Set.Finite.mem_toFinset` `Set.mem_compl_iff` `Set.mem_preimage` `SetLike.mem_coe` `Finset.disjoint_left`
`summable_iff_tendsto_cofinite_zero` 📖	mathematical	—	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional` `Filter.Tendsto` `Filter.cofinite` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Summable.tendsto_cofinite_zero` `toIsTopologicalAddGroup` `summable_of_tendsto_cofinite_zero`
`summable_of_tendsto_cofinite_zero` 📖	mathematical	`Filter.Tendsto` `Filter.cofinite` `nhds` `UniformSpace.toTopologicalSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Summable` `AddCommGroup.toAddCommMonoid` `SummationFilter.unconditional`	—	`CompleteSpace.complete` `cauchySeq_sum_of_tendsto_cofinite_zero`

NonarchimedeanGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchySeq_of_tendsto_div_nhds_one` 📖	mathematical	`Filter.Tendsto` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`CauchySeq`	—	`Filter.tendsto_atTop'` `SemilatticeSup.instIsDirectedOrder` `is_nonarchimedean` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.tendsto_def` `OpenSubgroup.mem_nhds_one` `add_zero` `div_self'` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `OpenSubgroup.instSubgroupClass` `div_mul_div_cancel` `Subgroup.mul_mem` `inv_div` `Subgroup.inv_mem` `le_of_not_ge` `Filter.prod_atTop_atTop_eq` `uniformity_eq_comap_nhds_one` `IsUniformGroup.isRightUniformGroup`
`cauchySeq_prod_of_tendsto_cofinite_one` 📖	mathematical	`Filter.Tendsto` `Filter.cofinite` `nhds` `UniformSpace.toTopologicalSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`CauchySeq` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Finset.prod` `CommGroup.toCommMonoid`	—	`cauchySeq_finset_iff_prod_vanishing` `is_nonarchimedean` `Filter.tendsto_def` `OpenSubgroup.mem_nhds_one` `Subgroup.prod_mem` `Finset.disjoint_left`
`multipliable_iff_tendsto_cofinite_one` 📖	mathematical	—	`Multipliable` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional` `Filter.Tendsto` `Filter.cofinite` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`Multipliable.tendsto_cofinite_one` `toIsTopologicalGroup` `multipliable_of_tendsto_cofinite_one`
`multipliable_of_tendsto_cofinite_one` 📖	mathematical	`Filter.Tendsto` `Filter.cofinite` `nhds` `UniformSpace.toTopologicalSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`Multipliable` `CommGroup.toCommMonoid` `SummationFilter.unconditional`	—	`CompleteSpace.complete` `cauchySeq_prod_of_tendsto_cofinite_one`

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_of_nonarchimedean` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`HasSum.summable` `HasSum.mul_of_nonarchimedean` `hasSum`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tsum_mul_tsum_of_nonarchimedean` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `tsum`	—	`HasSum.tsum_eq` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `IsTopologicalAddGroup.regularSpace` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `NonarchimedeanRing.to_nonarchimedeanAddGroup` `SummationFilter.instNeBotUnconditional` `HasSum.mul_of_nonarchimedean` `Summable.hasSum`

---

← Back to Index