Theorem Multipliable.norm

Modification history

2024-11-11 09:44

Mathlib/Topology/Algebra/InfiniteSum/Field.lean

feat(InfiniteSum): infinite product of absolute value (#18747)

Added Multipliable.norm View on Github →