Attribute the multiplication theorem proof

girving · Jan 4, 2025 · 9d1e966 · 9d1e966
1 parent e366b3b
commit 9d1e966
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Interval/EulerMaclaurin/Bernoulli.lean b/Interval/EulerMaclaurin/Bernoulli.lean
@@ -146,6 +146,7 @@ lemma integrable_bernoulliFun_comp_add_right {s : ℕ} {a b c : ℝ} :
   apply Continuous.intervalIntegrable
   continuity
 
+/-- The multiplication theorem. Proof follows https://math.stackexchange.com/a/1721099/38218. -/
 lemma bernoulliFun_mul (s m : ℕ) (m0 : m ≠ 0) (x : ℝ) :
     bernoulliFun s (m * x) =
       m ^ s / m * ∑ k ∈ Finset.range m, bernoulliFun s (x + k / m) := by