Minimize imports to make Sum.lean much faster

Changes

1 changed files (+5/-2)

• Sum.lean
  • @@ -1,5 +1,8 @@
    - import Mathlib - open Finset BigOperators Filter Topology + import Mathlib.Algebra.Field.GeomSum + import Mathlib.Analysis.RCLike.Basic + import Mathlib.Tactic.IntervalCases + import Mathlib.Tactic.Rify + open Finset Filter Topology -- Important: b should be in ℝ so that it's real div not nat div lemma geom_sum (N : ℕ) (b : ℝ) (hN : 2 ≤ N) (hb : 2 ≤ b) : ∑ a ∈ Ico 2 N, 1 / (b ^ a) = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) :=