PSeriesComplex

Statistics

Metric	Count
Definitions	0
Theorems `summable_one_div_nat_cpow`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`summable_one_div_nat_cpow` 📖	mathematical	—	`Summable` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instPow` `instNatCast` `SummationFilter.unconditional` `Real` `Real.instLT` `Real.instOne` `re`	—	`Real.summable_one_div_nat_rpow` `summable_nat_add_iff` `instIsTopologicalAddGroupReal` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `summable_norm_iff` `instFiniteDimensionalReal` `norm_div` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `norm_cpow_eq_rpow_re_of_pos` `Nat.cast_pos` `Real.instIsOrderedRing` `Real.instNontrivial`

---