Theorem Complex.le_of_eq_sum_of_eq_sum_norm

Modification history

2024-07-25 17:03
Mathlib/Analysis/Complex/Basic.lean
feat(Analysis/Complex): If `a = ∑ i ∈ s, f i` and `b = ∑ i ∈ s, (‖f i‖ : ℂ)`, then `a ≤ b` (#15022) …
Added Complex.le_of_eq_sum_of_eq_sum_normView on Github →