We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent c8f6dda commit c686dc0Copy full SHA for c686dc0
1 file changed
Mathlib/Combinatorics/Enumerative/PentagonalNumbers.lean
@@ -263,4 +263,4 @@ lemma coeff_E_eq_coeff_cutoff (n : ℕ) :
263
(PowerSeries.coeff n) (E n) =
264
(PowerSeries.coeff n)
265
(∏ k ∈ Finset.range (n + 1), (1 - (PowerSeries.X : PowerSeries ℤ) ^ (k + 1))) := by
266
- simp [E]
+ rfl
0 commit comments