Field

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

Statistics

Metric	Count
Definitions	0
Theorems norm, norm, norm_tprod	3
Total	3

HasProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm 📖	mathematical	HasProd CommRing.toCommMonoid SeminormedCommRing.toCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing SummationFilter.unconditional	Real Real.instCommMonoid Real.pseudoMetricSpace Norm.norm SeminormedRing.toNorm	—	Finset.prod_congr Filter.Tendsto.norm

Multipliable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm 📖	mathematical	Multipliable CommRing.toCommMonoid SeminormedCommRing.toCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing SummationFilter.unconditional	Real Real.instCommMonoid Real.pseudoMetricSpace Norm.norm SeminormedRing.toNorm	—	HasProd.norm
norm_tprod 📖	mathematical	Multipliable CommRing.toCommMonoid SeminormedCommRing.toCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing SummationFilter.unconditional	Norm.norm SeminormedRing.toNorm tprod Real Real.instCommMonoid Real.pseudoMetricSpace	—	HasProd.tprod_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional HasProd.norm hasProd

---

← Back to Index