chore(number_theory/bernoulli_polynomials): tidy docs (#16705)

ericrbg · kim-em · ericrbg · commit ca3d21f7f4fd · 2022-11-18T10:49:31.000Z
Co-authored-by: Scott Morrison &lt;scott@tqft.net&gt;
diff --git a/src/number_theory/bernoulli_polynomials.lean b/src/number_theory/bernoulli_polynomials.lean
@@ -196,7 +196,7 @@ variables {A : Type*} [comm_ring A] [algebra ℚ A]
 -- TODO: define exponential generating functions, and use them here
 -- This name should probably be updated afterwards
 
-/-- The theorem that `∑ Bₙ(t)X^n/n!)(e^X-1)=Xe^{tX}`  -/
+/-- The theorem that $(e^X - 1) * ∑ Bₙ(t)* X^n/n! = Xe^{tX}$ -/
 theorem bernoulli_generating_function (t : A) :
   mk (λ n, aeval t ((1 / n! : ℚ) • bernoulli n)) * (exp A - 1) =
     power_series.X * rescale t (exp A) :=
