Skip to content

Commit 805e37b

Browse files
wwylelewwylele
committed
feat(PowerSeries): pentagonal number theorem (leanprover-community#33143)
The proof is split in two files: `Mathlib/Combinatorics/Enumerative/Ring.lean` for the algebraic part, and `Mathlib/Combinatorics/Enumerative/PowerSeries.lean` for the summability part. In the near future, I also plan to prove the real/complex version that branches off from the algebraic part.
1 parent 5e63835 commit 805e37b

6 files changed

Lines changed: 360 additions & 7 deletions

File tree

‎Mathlib.lean‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3561,7 +3561,9 @@ public import Mathlib.Combinatorics.Enumerative.InclusionExclusion
35613561
public import Mathlib.Combinatorics.Enumerative.Partition.Basic
35623562
public import Mathlib.Combinatorics.Enumerative.Partition.GenFun
35633563
public import Mathlib.Combinatorics.Enumerative.Partition.Glaisher
3564-
public import Mathlib.Combinatorics.Enumerative.Pentagonal
3564+
public import Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
3565+
public import Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
3566+
public import Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
35653567
public import Mathlib.Combinatorics.Enumerative.Schroder
35663568
public import Mathlib.Combinatorics.Enumerative.Stirling
35673569
public import Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Mathlib/Combinatorics/Enumerative/Pentagonal.lean renamed to Mathlib/Combinatorics/Enumerative/Pentagonal/Basic.lean

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -21,11 +21,6 @@ convention, but implicitly shows the monotonicity in `pentagonal_lt_pentagonal_n
2121
2222
* `pentagonal`: pentagonal numbers as a function `ℤ → ℕ`.
2323
24-
## TODO
25-
26-
Show the relation between pentagonal numbers and partitions, including the pentagonal number
27-
theorem.
28-
2924
## References
3025
3126
* https://en.wikipedia.org/wiki/Pentagonal_number

‎Mathlib/Combinatorics/Enumerative/Pentagonal/PowerSeries.lean‎

Lines changed: 184 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,184 @@
1+
/-
2+
Copyright (c) 2025 Weiyi Wang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Weiyi Wang
5+
-/
6+
module
7+
8+
public import Mathlib.Algebra.Ring.NegOnePow
9+
public import Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
10+
public import Mathlib.RingTheory.PowerSeries.PiTopology
11+
12+
import Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
13+
import Mathlib.RingTheory.Nilpotent.Basic
14+
15+
/-!
16+
# Pentagonal number theorem for power series
17+
18+
This file proves the pentagonal number theorem for power series:
19+
20+
$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) = \sum_{k=-\infty}^{\infty} (-1)^k x^{a_k} $$
21+
22+
where $a_k = k(3k - 1)/2$ are the pentagonal numbers. We state the theorem in two parts by
23+
introducing the intermediate power series `PowerSeries.pentagonalSeries`, whose coefficients are
24+
defined using pentagonal numbers. We then show that this series is equal to both sides.
25+
26+
## Main theorems
27+
28+
* `PowerSeries.WithPiTopology.hasProd_one_sub_X_pow`: `PowerSeries.pentagonalSeries` is equal to
29+
infinite product on the left-hand side of the formula.
30+
* `PowerSeries.coeff_prod_one_sub_X_pow_eventually_eq` restates the left-hand side without requiring
31+
topology.
32+
* `PowerSeries.WithPiTopology.hasSum_pentagonalSeries`: `PowerSeries.pentagonalSeries` is equal to
33+
the infinite sum on the right-hand side of the formula.
34+
* `PowerSeries.coeff_pentagonalSeries` restates the right-hand side without requiring topology.
35+
-/
36+
37+
open Filter PowerSeries WithPiTopology Topology
38+
variable (R : Type*) [CommRing R]
39+
40+
namespace Pentagonal
41+
-- private auxiliary lemma
42+
43+
theorem tendsto_order_pow_mul_prod_one_sub_pow (k : ℕ) :
44+
Tendsto (fun n ↦ (X ^ ((k + 1) * n) *
45+
∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)) : R⟦X⟧).order) atTop (𝓝 ⊤) := by
46+
nontriviality R using Subsingleton.eq_zero
47+
refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr fun n ↦ eventually_atTop.mpr ⟨n + 1, ?_⟩
48+
intro m hm
49+
grw [← le_order_mul, order_X_pow]
50+
refine lt_add_of_lt_of_nonneg ?_ (by simp)
51+
norm_cast
52+
grind
53+
54+
theorem tendsto_order_neg_X_pow (k : ℕ) :
55+
Tendsto (fun i ↦ (-(X : R⟦X⟧) ^ (i + k + 1)).order) atTop (𝓝 ⊤) := by
56+
nontriviality R using Subsingleton.eq_zero
57+
simp_rw [order_neg, order_X_pow, add_assoc]
58+
exact ENat.tendsto_natCast_nhds_top.comp (tendsto_add_atTop_nat _)
59+
60+
variable [TopologicalSpace R]
61+
62+
theorem summable_pow_mul_prod_one_sub_pow (k : ℕ) :
63+
Summable
64+
fun n ↦ (X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)) : R⟦X⟧) :=
65+
summable_of_tendsto_order_atTop_nhds_top R (tendsto_order_pow_mul_prod_one_sub_pow R k)
66+
67+
theorem multipliable_one_sub_X_pow (k : ℕ) : Multipliable fun n ↦ (1 : R⟦X⟧) - X ^ (n + k + 1) := by
68+
simpa [sub_eq_add_neg] using
69+
multipliable_one_add_of_tendsto_order_atTop_nhds_top R (tendsto_order_neg_X_pow R k)
70+
71+
end Pentagonal
72+
73+
public section Public
74+
namespace PowerSeries
75+
76+
open Classical in
77+
/-- The power series $\sum_{k=-\infty}^{\infty}(-1)^k x^{k * (3k - 1) / 2}$. -/
78+
noncomputable
79+
def pentagonalSeries : R⟦X⟧ :=
80+
.mk fun n ↦ if h : ∃ k, pentagonal k = n then
81+
Int.negOnePow h.choose
82+
else
83+
0
84+
85+
theorem coeff_pentagonalSeries_eq_zero {n : ℕ} (h : n ∉ Set.range pentagonal) :
86+
(pentagonalSeries R).coeff n = 0 := dif_neg <| by simpa using h
87+
88+
@[simp]
89+
theorem coeff_pentagonalSeries_pentagonal (k : ℤ) :
90+
(pentagonalSeries R).coeff (pentagonal k) = Int.negOnePow k := by
91+
simp [pentagonalSeries]
92+
93+
@[simp]
94+
theorem coeff_pentagonalSeries_eq_zero_iff [Nontrivial R] {n : ℕ} :
95+
(pentagonalSeries R).coeff n = 0 ↔ n ∉ Set.range pentagonal := by
96+
grind [pentagonalSeries, coeff_mk, neg_one_pow_ne_zero, Int.coe_negOnePow]
97+
98+
namespace WithPiTopology
99+
variable [TopologicalSpace R]
100+
101+
/-- `PowerSeries.pentagonalSeries` as an infinite sum over integers -/
102+
theorem hasSum_pentagonalSeries :
103+
HasSum (fun k : ℤ ↦ (Int.negOnePow k : R⟦X⟧) * X ^ pentagonal k) (pentagonalSeries R) := by
104+
suffices HasSum ((fun n ↦ C ((pentagonalSeries R).coeff n) * X ^ n) ∘ pentagonal)
105+
(pentagonalSeries R) by
106+
convert this
107+
simp
108+
rw [pentagonal_injective.hasSum_iff fun n hn ↦ by simp [coeff_pentagonalSeries_eq_zero R hn]]
109+
simpa [monomial_eq_C_mul_X_pow] using (pentagonalSeries R).hasSum_of_monomials_self
110+
111+
theorem pentagonalSeries_eq_tsum [T2Space R] :
112+
pentagonalSeries R = ∑' k, (Int.negOnePow k : R⟦X⟧) * X ^ pentagonal k :=
113+
(hasSum_pentagonalSeries R).tsum_eq.symm
114+
115+
/-- `PowerSeries.pentagonalSeries` as an infinite sum over natural numbers. In this version, terms
116+
are ordered by strictly increasing exponent `pentagonal k` for `k = 0, 1, -1, 2, -2, 3, ...`,
117+
and every two terms are grouped together. -/
118+
theorem hasSum_pow_pentagonal_sub_pentagonalSeries :
119+
HasSum (fun k : ℕ ↦ (-1) ^ k * (X ^ pentagonal (-k) - X ^ pentagonal (k + 1)))
120+
(pentagonalSeries R) := by
121+
have h := hasSum_pentagonalSeries R
122+
rw [← neg_injective.hasSum_iff (fun x hx ↦ by absurd hx; use -x; simp)] at h
123+
convert h.nat_add_neg_add_one using 2 with k
124+
simp_rw [Function.comp_apply, neg_neg, Int.negOnePow_add]
125+
simp
126+
ring
127+
128+
theorem pentagonalSeries_eq_tsum_pow_pentagonal_sub [T2Space R] :
129+
pentagonalSeries R = ∑' (k : ℕ), (-1) ^ k * (X ^ pentagonal (-k) - X ^ pentagonal (k + 1)) :=
130+
(hasSum_pow_pentagonal_sub_pentagonalSeries R).tsum_eq.symm
131+
132+
/-- See the public version `PowerSeries.WithPiTopology.tprod_one_sub_X_pow` that removes
133+
`IsTopologicalRing`. -/
134+
private theorem tprod_one_sub_X_pow' [IsTopologicalRing R] [T2Space R] :
135+
∏' n, (1 - X ^ (n + 1) : R⟦X⟧) = pentagonalSeries R := by
136+
nontriviality R
137+
rw [pentagonalSeries_eq_tsum_pow_pentagonal_sub]
138+
refine Pentagonal.tprod_one_sub_pow ?_ ?_ ?_ ?_ ?_
139+
· rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto]
140+
refine fun d ↦ tendsto_atTop_of_eventually_const fun i (hi : i ≥ d + 1) ↦ ?_
141+
grind
142+
· exact Pentagonal.summable_pow_mul_prod_one_sub_pow R
143+
· exact Pentagonal.multipliable_one_sub_X_pow R
144+
· exact (hasSum_pow_pentagonal_sub_pentagonalSeries R).summable
145+
· rw [tendsto_iff_coeff_tendsto]
146+
refine fun n ↦ tendsto_atTop_of_eventually_const fun k (hk : k ≥ n) ↦ ?_
147+
rw [map_zero]
148+
apply coeff_of_lt_order
149+
grw [← le_order_mul, ← le_order_mul]
150+
refine (lt_add_of_lt_of_nonneg (lt_add_of_nonneg_of_lt (by simp) ?_) (by simp))
151+
rw [order_X_pow, Nat.cast_lt, ← Nat.add_one_le_iff, Nat.le_div_iff_mul_le (by simp)]
152+
apply Nat.mul_le_mul <;> linarith
153+
154+
end WithPiTopology
155+
156+
/-- **Pentagonal number theorem** for power series, expressed as the statement that the coefficients
157+
of the product `∏ n, 1 - X ^ (n + 1)` are eventually constants as `(pentagonalSeries R).coeff`. -/
158+
theorem coeff_prod_one_sub_X_pow_eventually_eq (n : ℕ) :
159+
∀ᶠ s in atTop, (∏ n ∈ s, (1 - X ^ (n + 1) : R⟦X⟧)).coeff n = (pentagonalSeries R).coeff n := by
160+
let : TopologicalSpace R := ⊥
161+
have : DiscreteTopology R := ⟨rfl⟩
162+
have h := (multipliable_one_sub_X_pow R).hasProd
163+
rw [tprod_one_sub_X_pow' R, HasProd, tendsto_iff_coeff_tendsto] at h
164+
simpa using h n
165+
166+
namespace WithPiTopology
167+
variable [TopologicalSpace R]
168+
169+
/-- **Pentagonal number theorem** for power series, expressed as an infinite product. See also
170+
`PowerSeries.WithPiTopology.hasSum_pentagonalSeries` that expresses `pentagonalSeries` as an
171+
infinite sum. -/
172+
theorem hasProd_one_sub_X_pow :
173+
HasProd (fun n ↦ (1 - X ^ (n + 1) : R⟦X⟧)) (pentagonalSeries R) := by
174+
rw [HasProd, tendsto_iff_coeff_tendsto]
175+
intro n
176+
apply tendsto_nhds_of_eventually_eq
177+
simpa using coeff_prod_one_sub_X_pow_eventually_eq R n
178+
179+
theorem tprod_one_sub_X_pow [T2Space R] : ∏' n, (1 - X ^ (n + 1) : R⟦X⟧) = pentagonalSeries R :=
180+
(hasProd_one_sub_X_pow R).tprod_eq
181+
182+
end WithPiTopology
183+
end PowerSeries
184+
end Public

‎Mathlib/Combinatorics/Enumerative/Pentagonal/Ring.lean‎

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
/-
2+
Copyright (c) 2025 Weiyi Wang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Weiyi Wang
5+
-/
6+
module
7+
8+
public import Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
9+
public import Mathlib.Topology.Algebra.InfiniteSum.Ring
10+
public import Mathlib.Topology.Algebra.TopologicallyNilpotent
11+
12+
/-!
13+
# Pentagonal number theorem
14+
15+
This is an intermediate file that proves the pentagonal number theorem in a general topological ring
16+
modulo summability and multipliability. The complete proof for formal power series is in
17+
`Mathlib/RingTheory/PowerSeries/Pentagonal.lean`. TODO: also prove for real/complex numbers.
18+
19+
## Declarations
20+
21+
* `Pentagonal.tprod_one_sub_pow`: pentagonal number theorem with a few summability and
22+
multipliability assumptions.
23+
24+
## References
25+
26+
https://math.stackexchange.com/questions/55738/how-to-prove-eulers-pentagonal-theorem-some-hints-will-help
27+
28+
-/
29+
30+
namespace Pentagonal
31+
open Filter Topology
32+
variable {R : Type*} [CommRing R]
33+
34+
/--
35+
We define an auxiliary sequence
36+
37+
$$ a_{k, n} = x^{(k+1)n} \prod_{i=0}^{n} (1 - x^{k + i + 1}) $$
38+
39+
We will also use its sum
40+
41+
$$ A_k = \sum_{n=0}^{\infty} a_{k, n} $$ -/
42+
def powMulProdOneSubPow (k n : ℕ) (x : R) : R :=
43+
x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
44+
45+
/-- And a second auxiliary sequence
46+
47+
$$ b_{k, n} = x^{(k+1)n} (x^{2k + n + 3} - 1) \prod_{i=0}^{n-1} (1 - x^{k + i + 2}) $$ -/
48+
def aux (k n : ℕ) (x : R) : R :=
49+
x ^ ((k + 1) * n) * (x ^ (2 * k + n + 3) - 1) * ∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))
50+
51+
/-- `powMulProdOneSubPow` and `aux` have relation
52+
53+
$$ a_{k,n} + x^{3k + 5}a_{k + 1, n} = b_{k, n+1} - b_{k, n} $$ -/
54+
theorem aux_sub_aux (k n : ℕ) (x : R) :
55+
powMulProdOneSubPow k n x + x ^ (3 * k + 5) * powMulProdOneSubPow (k + 1) n x =
56+
aux k (n + 1) x - aux k n x := by
57+
simp_rw [aux, Finset.prod_range_succ, powMulProdOneSubPow]
58+
rw [Finset.prod_range_succ', Finset.prod_range_succ]
59+
ring_nf
60+
61+
variable [TopologicalSpace R] [IsTopologicalRing R] [T2Space R]
62+
63+
/-- By summing with telescoping, we get a recurrence formula for $A$
64+
65+
$$ A_k = 1 - x^{2k + 3} - x^{3k + 5}A_{k + 1} $$
66+
-/
67+
theorem tsum_powMulProdOneSubPow (k : ℕ) {x : R} (hx : IsTopologicallyNilpotent x)
68+
(hsum : ∀ k, Summable (powMulProdOneSubPow k · x))
69+
(h : ∀ k, Multipliable (fun n ↦ 1 - x ^ (n + k + 1))) :
70+
∑' n, powMulProdOneSubPow k n x =
71+
1 - x ^ (2 * k + 3) - x ^ (3 * k + 5) * ∑' n, powMulProdOneSubPow (k + 1) n x := by
72+
rw [eq_sub_iff_add_eq, show 1 - x ^ (2 * k + 3) = 0 - aux k 0 x by simp [aux]]
73+
rw [← (hsum _).tsum_mul_left, ← (hsum _).tsum_add ((hsum _).mul_left _)]
74+
apply HasSum.tsum_eq
75+
rw [((hsum _).add ((hsum _).mul_left _)).hasSum_iff_tendsto_nat]
76+
simp_rw [aux_sub_aux, Finset.sum_range_sub (aux k · x)]
77+
apply Tendsto.sub_const
78+
rw [show 𝓝 0 = 𝓝 (0 * (0 - 1) * ∏' i, (1 - x ^ (k + i + 2))) by simp]
79+
refine (Tendsto.mul ?_ ?_).mul ?_
80+
· exact hx.comp (strictMono_mul_left_of_pos (by simp)).tendsto_atTop
81+
· exact (hx.comp (add_right_strictMono.add_monotone monotone_const).tendsto_atTop).sub_const _
82+
· apply Multipliable.tendsto_prod_tprod_nat
83+
convert h (k + 1) using 4
84+
ring
85+
86+
/-- The Euler function is related to $A_0$ by
87+
88+
$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) = 1 - x - x^2 A_0 $$ -/
89+
theorem tprod_one_sub_pow_eq_powMulProdOneSubPow_zero {x : R}
90+
(hsum : ∀ k, Summable (powMulProdOneSubPow k · x))
91+
(h : ∀ k, Multipliable fun n ↦ 1 - x ^ (n + k + 1)) :
92+
∏' n, (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' n, powMulProdOneSubPow 0 n x := by
93+
have hsum := hsum 0
94+
simp_rw [powMulProdOneSubPow, zero_add, one_mul] at hsum
95+
have hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1)) := by
96+
apply Summable.comp_nat_add (k := 1)
97+
conv in fun k ↦ _ =>
98+
ext k
99+
rw [pow_add, pow_add, mul_assoc (x ^ k), mul_comm (x ^ k), mul_assoc (x ^ 1 * x ^ 1)]
100+
exact hsum.mul_left _
101+
rw [tprod_one_sub_ordered (by simpa [Nat.Iio_eq_range] using hsum') (by simpa using h 0)]
102+
simp_rw [Nat.Iio_eq_range, sub_sub, sub_right_inj, hsum'.tsum_eq_zero_add]
103+
conv in fun k ↦ x ^ (k + 1 + 1) * _ =>
104+
ext k
105+
rw [pow_add, pow_add, mul_assoc (x ^ k), mul_comm (x ^ k),
106+
← pow_add x 1 1, one_add_one_eq_two, mul_assoc (x ^ 2)]
107+
simp [hsum.tsum_mul_left, powMulProdOneSubPow]
108+
109+
/-- Applying the recurrence formula repeatedly, we get
110+
111+
$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) =
112+
\left(\sum_{k=0}^{j} (-1)^k \left(x^{k(3k+1)/2} - x^{(k+1)(3k+2)/2}\right) \right) +
113+
(-1)^{j+1}x^{(j+1)(3j+4)/2}A_j $$ -/
114+
theorem tprod_one_sub_pow_eq_powMulProdOneSubPow (j : ℕ) {x : R} (hx : IsTopologicallyNilpotent x)
115+
(hsum : ∀ k, Summable (powMulProdOneSubPow k · x))
116+
(h : ∀ k, Multipliable (fun n ↦ 1 - x ^ (n + k + 1))) :
117+
∏' n, (1 - x ^ (n + 1)) = ∑ k ∈ Finset.range (j + 1),
118+
(-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))
119+
+ (-1) ^ (j + 1) * x ^ ((j + 1) * (3 * j + 4) / 2) * ∑' n, powMulProdOneSubPow j n x := by
120+
induction j with
121+
| zero =>
122+
simp [tprod_one_sub_pow_eq_powMulProdOneSubPow_zero hsum h, powMulProdOneSubPow,
123+
← sub_eq_add_neg]
124+
| succ n ih =>
125+
rw [ih, tsum_powMulProdOneSubPow _ hx hsum h, Finset.sum_range_succ _ (n + 1)]
126+
have h (n) : (n + 1 + 1) * (3 * (n + 1) + 2) / 2 =
127+
(n + 1) * (3 * n + 4) / 2 + (2 * n + 3) := by
128+
rw [← Nat.add_mul_div_left _ _ (by simp)]
129+
ring_nf
130+
simp_rw [h]
131+
have h (n) : (n + 1 + 1) * (3 * (n + 1) + 4) / 2 =
132+
(n + 1) * (3 * n + 4) / 2 + (3 * n + 5) := by
133+
rw [← Nat.add_mul_div_left _ _ (by simp)]
134+
ring_nf
135+
simp_rw [h]
136+
ring_nf
137+
138+
/-- **Pentagonal number theorem**, assuming appropriate multipliability and summability.
139+
140+
$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) =
141+
\sum_{k=0}^{\infty} (-1)^k \left(x^{k(3k+1)/2} - x^{(k+1)(3k+2)/2}\right) $$ -/
142+
public theorem tprod_one_sub_pow {x : R} (hx : IsTopologicallyNilpotent x)
143+
(hsum : ∀ k, Summable
144+
(fun n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))))
145+
(hlhs : ∀ k, Multipliable (fun n ↦ 1 - x ^ (n + k + 1)))
146+
(hrhs : Summable fun k : ℕ ↦
147+
(-1) ^ k * (x ^ pentagonal (-k) - x ^ pentagonal (k + 1)))
148+
(htail : Tendsto (fun k ↦ (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
149+
∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
150+
atTop (𝓝 0)) :
151+
∏' n, (1 - x ^ (n + 1)) =
152+
∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-k) - x ^ pentagonal (k + 1)) := by
153+
have h := fun n ↦ tprod_one_sub_pow_eq_powMulProdOneSubPow n hx hsum hlhs
154+
simp_rw [← sub_eq_iff_eq_add] at h
155+
refine (HasSum.tsum_eq ?_).symm
156+
rw [hrhs.hasSum_iff_tendsto_nat, (map_add_atTop_eq_nat 1).symm]
157+
apply tendsto_map'
158+
have h1 (k : ℕ) : pentagonal (k + 1) = ((k + 1) * (3 * k + 2) / 2) := by grind [pentagonal_def]
159+
have h2 (k : ℕ) : pentagonal (-k) = (k * (3 * k + 1) / 2) := by grind [pentagonal_neg]
160+
simp_rw [h1, h2, Function.comp_def, ← h]
161+
rw [← tendsto_sub_nhds_zero_iff]
162+
simpa [powMulProdOneSubPow] using htail.neg
163+
164+
end Pentagonal

‎Mathlib/RingTheory/Nilpotent/Basic.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,14 @@ theorem IsNilpotent.neg [Ring R] (h : IsNilpotent x) : IsNilpotent (-x) := by
4444
use n
4545
rw [neg_pow, hn, mul_zero]
4646

47+
theorem not_isNilpotent_neg_one [Ring R] [Nontrivial R] : ¬ IsNilpotent (-1 : R) := by
48+
intro h
49+
simpa [not_isNilpotent_one] using h.neg
50+
51+
theorem neg_one_pow_ne_zero [Ring R] [Nontrivial R] (n : ℕ) : (-1 : R) ^ n ≠ 0 := by
52+
intro h
53+
exact not_isNilpotent_neg_one ⟨n, h⟩
54+
4755
@[simp]
4856
theorem isNilpotent_neg_iff [Ring R] : IsNilpotent (-x) ↔ IsNilpotent x :=
4957
⟨fun h => neg_neg x ▸ h.neg, fun h => h.neg⟩

‎docs/1000.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -323,7 +323,7 @@ Q282331:
323323

324324
Q282649:
325325
title: Pentagonal number theorem
326-
url: https://github.com/wwylele/PentagonalNumberTheorem
326+
decl: PowerSeries.WithPiTopology.hasProd_one_sub_X_pow
327327
authors: Weiyi Wang
328328
comment: Formal power series only. Missing power series over complex numbers.
329329
date: 2025-08-24

0 commit comments

Comments
 (0)