Commit 2024-07-25 17:03 799c0d47
View on Github →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