refactor(analysis/analytic/basic): redefine `formal_multilinear_serie…

…s.radius` (#5349) With the new definition, (a) some proofs get much shorter; (b) we don't need `rpow` in `analytic/basic`.
leanprover-community · Dec 31, 2020 · 0830bfd · 0830bfd
1 parent 10f6c15
commit 0830bfd
Show file tree

Hide file tree

Showing 5 changed files with 264 additions and 290 deletions.
diff --git a/src/algebra/big_operators/order.lean b/src/algebra/big_operators/order.lean
@@ -245,7 +245,6 @@ prod_induction f (λ x, 0 ≤ x) (λ _ _ ha hb, mul_nonneg ha hb) zero_le_one h0
 lemma prod_pos {s : finset α} {f : α → β} (h0 : ∀(x ∈ s), 0 < f x) : 0 < (∏ x in s, f x) :=
 prod_induction f (λ x, 0 < x) (λ _ _ ha hb, mul_pos ha hb) zero_lt_one h0
 
-
 /- this is also true for a ordered commutative multiplicative monoid -/
 lemma prod_le_prod {s : finset α} {f g : α → β} (h0 : ∀(x ∈ s), 0 ≤ f x)
   (h1 : ∀(x ∈ s), f x ≤ g x) : (∏ x in s, f x) ≤ (∏ x in s, g x) :=