Commit 2024-07-25 17:03 799c0d47

feat(Analysis/Complex): If a = ∑ i ∈ s, f i and b = ∑ i ∈ s, (‖f i‖ : ℂ), then a ≤ b (#15022) This is a bit of a weird statement, but it is really useful when one wants to expand ‖f i‖ = ‖g i‖ ^ 2 = g i * conj (g i) and do further complex number manipulations. It also avoids having to prove a = ∑ i ∈ s, f i twice: once for showing 0 ≤ a and once in the goal. From LeanAPAP