Commit 2024-11-11 09:44 2eb40bed

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Basic.lean

added theorem Complex.abs_tprod

added theorem Complex.hasProd_abs

added theorem Complex.multipliable_abs

Created Mathlib/Topology/Algebra/InfiniteSum/Field.lean

added theorem Multipliable.norm

added theorem norm_tprod

Modified Mathlib/Topology/Algebra/InfiniteSum/Order.lean

added theorem Multipliable.abs

added theorem abs_tprod