Theorem Complex.multipliable_abs

Modification history

2025-02-24 10:06
Mathlib/Analysis/Complex/Basic.lean
chore(Data/Complex): deprecate `Complex.abs` (#21995) …
Deleted Complex.multipliable_absView on Github →
2024-11-11 09:44
Mathlib/Analysis/Complex/Basic.lean
feat(InfiniteSum): infinite product of absolute value (#18747)
Added Complex.multipliable_absView on Github →