feat(Algebra/Group /ForwardDiff.lean): add five theorems for forward difference #26793

FlAmmmmING · 2025-07-05T16:37:27Z

feat(Combinatorics/Enumerative/Bell.lean): Add definitions of standrad bell number

github-actions · 2025-07-05T16:38:34Z

PR summary 063d2e5dac

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ fwdDiff_iter_eq_factorial
+ fwdDiff_iter_pow_eq_zero_of_lt
+ fwdDiff_iter_succ_sum_eq_zero
+ sum_fwdDiff_iter_at_zero
+ sum_of_poly_sequence

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

madvorak

Very nice results!

madvorak · 2025-07-06T15:29:56Z

Mathlib/Algebra/Group/ForwardDiff.lean

+degree `p` is zero.
+-/
+theorem fwdDiff_iter_pow_lt {x j n : ℕ} (h : j < n):
+  Δ_[1] ^[n] (fun x ↦ x ^ j : ℕ → R) x = (fun _ ↦  0) x := by


Suggested change

Δ_[1] ^[n] (fun x ↦ x ^ j : ℕ → R) x = (fun _ ↦ 0) x := by

Δ_[1] ^[n] (fun x ↦ x ^ j : ℕ → R) x = (fun _ ↦ 0) x := by

madvorak · 2025-07-06T15:30:19Z

Mathlib/Algebra/Group/ForwardDiff.lean

+theorem fwdDiff_iter_pow_lt {x j n : ℕ} (h : j < n):
+  Δ_[1] ^[n] (fun x ↦ x ^ j : ℕ → R) x = (fun _ ↦  0) x := by
+  revert j
+  induction' n with n IH


I suggest to not capitalize ih.

madvorak · 2025-07-06T15:30:29Z

Mathlib/Algebra/Group/ForwardDiff.lean

+    simp only [Int.reduceNeg, smul_eq_mul, mul_one, zsmul_eq_mul, Int.cast_mul,
+      Int.cast_pow, Int.cast_neg, Int.cast_one, Int.cast_natCast]
+    simp [fwdDiff_iter_eq_sum_shift] at IH
+    conv_lhs=> enter[2]; ext k; enter[2]; rw [fwdDiff, ← Nat.cast_pow,


Suggested change

conv_lhs=> enter[2]; ext k; enter[2]; rw [fwdDiff, ← Nat.cast_pow,

conv_lhs => enter[2]; ext k; enter[2]; rw [fwdDiff, ← Nat.cast_pow,

madvorak · 2025-07-06T15:30:39Z

Mathlib/Algebra/Group/ForwardDiff.lean

+
+/-- The `n`-th forward difference of `x ↦ x^n` is the constant function `n!`. -/
+theorem fwdDiff_iter_eq_factorial {n x : ℕ} :
+   Δ_[1] ^[n] (fun x ↦ x ^ n : ℕ → R) x = (fun _ ↦  n.factorial) x := by


Suggested change

Δ_[1] ^[n] (fun x ↦ x ^ n : ℕ → R) x = (fun _ ↦ n.factorial) x := by

Δ_[1] ^[n] (fun x ↦ x ^ n : ℕ → R) x = (fun _ ↦ n.factorial) x := by

madvorak · 2025-07-06T15:30:55Z

Mathlib/Algebra/Group/ForwardDiff.lean

+    simp [fwdDiff_iter_eq_sum_shift] at IH
+    conv_lhs=> enter[2]; ext k; enter[2]; rw [fwdDiff, ← Nat.cast_pow,
+      ← Nat.cast_pow, ← Nat.cast_sub (by apply Nat.pow_le_pow_left; linarith)]
+    conv_lhs=> enter[2];ext k;enter[2,1,1]; rw [add_pow, Finset.sum_range_succ]


Suggested change

conv_lhs=> enter[2];ext k;enter[2,1,1]; rw [add_pow, Finset.sum_range_succ]

conv_lhs => enter[2];ext k;enter[2,1,1]; rw [add_pow, Finset.sum_range_succ]

madvorak · 2025-07-06T15:31:26Z

Mathlib/Algebra/Group/ForwardDiff.lean

+      ← Nat.cast_pow, ← Nat.cast_sub (by apply Nat.pow_le_pow_left; linarith)]
+    conv_lhs=> enter[2];ext k;enter[2,1,1]; rw [add_pow, Finset.sum_range_succ]
+    simp only [one_pow, mul_one, Nat.cast_id, tsub_self, pow_zero, Nat.choose_self, Nat.cast_one]
+    conv_lhs=> enter[2]; ext k; enter[2, 1]; rw [Nat.add_sub_cancel_right]


Suggested change

conv_lhs=> enter[2]; ext k; enter[2, 1]; rw [Nat.add_sub_cancel_right]

conv_lhs => enter[2]; ext k; enter[2, 1]; rw [Nat.add_sub_cancel_right]

madvorak · 2025-07-06T15:31:33Z

Mathlib/Algebra/Group/ForwardDiff.lean

+    conv_lhs=> enter[2];ext k;enter[2,1,1]; rw [add_pow, Finset.sum_range_succ]
+    simp only [one_pow, mul_one, Nat.cast_id, tsub_self, pow_zero, Nat.choose_self, Nat.cast_one]
+    conv_lhs=> enter[2]; ext k; enter[2, 1]; rw [Nat.add_sub_cancel_right]
+    conv_lhs=> enter [2]; ext k; rw [mul_assoc, ← Nat.cast_mul, Finset.mul_sum]


Suggested change

conv_lhs=> enter [2]; ext k; rw [mul_assoc, ← Nat.cast_mul, Finset.mul_sum]

conv_lhs => enter [2]; ext k; rw [mul_assoc, ← Nat.cast_mul, Finset.mul_sum]

madvorak · 2025-07-06T15:32:17Z

Mathlib/Algebra/Group/ForwardDiff.lean

+-/
+theorem fwdDiff_iter_succ_sum_eq_zero {n x : ℕ} (a : ℕ → R):
+    Δ_[1] ^[n + 1] (fun (x : ℕ) =>
+      ∑ k ∈ Finset.range (n + 1), a k • (x ^ k) : ℕ → R) x  = (fun _ ↦ 0) x := by


Why • here?

Dtto below.

madvorak · 2025-07-06T15:32:33Z

Mathlib/Algebra/Group/ForwardDiff.lean

+theorem fwdDiff_iter_succ_sum_eq_zero {n x : ℕ} (a : ℕ → R):
+    Δ_[1] ^[n + 1] (fun (x : ℕ) =>
+      ∑ k ∈ Finset.range (n + 1), a k • (x ^ k) : ℕ → R) x  = (fun _ ↦ 0) x := by
+  induction' n with n IH


Again, I suggest ih.

madvorak · 2025-07-06T15:33:24Z

Mathlib/Algebra/Group/ForwardDiff.lean

+`f(x) = ∑_{k=0..x} (x choose k) * (Δ^k f)(0)`.
+-/
+theorem fwdDiffTab_0th_diag_poly' {n x : ℕ} (a : ℕ → R[X]):
+  (∑ k ∈ Finset.range (n + 1), a k • (x ^ k) : R[X]) =


Suggested change

(∑ k ∈ Finset.range (n + 1), a k • (x ^ k) : R[X]) =

(∑ k ∈ Finset.range (n + 1), a k • (x ^ k) : R[X]) =

madvorak · 2025-07-06T15:36:17Z

Mathlib/Algebra/Group/ForwardDiff.lean

+    obtain sum_choose := h₁ p
+    conv => enter [1, 2, x]; rw [fwdDiffTab_0th_diag_poly']; simp
+    simp only [smul_eq_mul]
+    have h₂ : ∑ x ∈ Finset.range (p + 1), ∑ x_1 ∈ Finset.range (x + 1),


Please replace x_1 and h₂ by better names.

madvorak · 2025-07-06T15:36:53Z

Mathlib/Algebra/Group/ForwardDiff.lean

+        rw [Nat.choose_eq_zero_of_lt this]
+        simp
+      nth_rw 1 3 [Finset.range_eq_Ico]
+      have h₁₂ : ∑ x_1 ∈ Finset.Ico 0 (p + 1), ↑(x.choose x_1) * Δ_[1] ^[x_1]


Please replace x_1 and h₁₂ by better names.

Thank you for your patience! I will make the changes based on your suggestions!

kckennylau · 2025-07-07T14:02:12Z

Mathlib/Algebra/Group/ForwardDiff.lean

+theorem fwdDiff_iter_pow_lt {x j n : ℕ} (h : j < n):
+  Δ_[1] ^[n] (fun x ↦ x ^ j : ℕ → R) x = (fun _ ↦ 0) x := by
+  revert j
+  induction' n with n ih
+  · simp only [not_lt_zero', Function.iterate_zero, id_eq,
+      IsEmpty.forall_iff, implies_true]
+  · intro j hj
+    rw [Function.iterate_succ, Function.comp_apply, fwdDiff_iter_eq_sum_shift]
+    simp only [Int.reduceNeg, smul_eq_mul, mul_one, zsmul_eq_mul, Int.cast_mul,
+      Int.cast_pow, Int.cast_neg, Int.cast_one, Int.cast_natCast]
+    simp [fwdDiff_iter_eq_sum_shift] at ih
+    conv_lhs => enter[2]; ext k; enter[2]; rw [fwdDiff, ← Nat.cast_pow,
+      ← Nat.cast_pow,← Nat.cast_sub (by apply Nat.pow_le_pow_left; linarith),
+      add_pow, Finset.sum_range_succ]
+    simp only [one_pow, mul_one, Nat.cast_id,
+      tsub_self, pow_zero, Nat.choose_self, Nat.cast_one]
+    conv_lhs=> enter[2]; ext k; rw [Nat.add_sub_cancel_right (m := (x + k) ^ j),
+      mul_assoc, ← Nat.cast_mul, Finset.mul_sum]
+    norm_num
+    simp [Finset.mul_sum, Finset.sum_comm, ← mul_assoc, ← mul_assoc, ← Finset.sum_mul]
+    rw [Finset.sum_eq_zero]
+    intro k hk; simp only [Finset.mem_range] at hk
+    rw [ih (by linarith)]
+    simp


You should first generalise this theorem to x taking value in R, which will give you a much more efficient proof (with one sorry here left as exercise):

theorem fwdDiff_iter_pow_eq_zero_of_lt {j n : ℕ} (h : j < n) : ((fwdDiffₗ R R 1 ^ n) fun x ↦ x ^ j) = 0 := by induction' n with n ih generalizing j · contradiction · rw [pow_succ, Module.End.mul_apply] have : ((fwdDiffₗ R R 1) fun x ↦ x ^ j) = ∑ i ∈ Finset.range j, j.choose i • fun x : R ↦ x ^ i := by ext x; simp; sorry rw [this, map_sum] exact sum_eq_zero fun i hi ↦ have _ := mem_range.1 hi; by rw [map_nsmul, ih (by omega)]; simp

AntoineChambert-Loir · 2025-07-10T22:24:27Z

Mathlib/Algebra/Group/ForwardDiff.lean

+open fwdDiff
+variable {R : Type*} [CommRing R]
+
+/--


For this statement and the two that follow, it would help to first prove the following lemma: if p is a polynomial of degree <= n + 1, with coefficient of degree (n + 1) equal to a, , then fwdDiffₗ R R 1 is a polynomial of degree <= n whose coefficient of degree n is equal to (n + 1) * a. Then all inductions should be effortless.

AntoineChambert-Loir · 2025-07-10T22:29:35Z

Mathlib/Algebra/Group/ForwardDiff.lean

+    ∑ i ∈ Finset.range (p + 1), (∑ k ∈ Finset.range (n + 1), a k * i ^ k) =
+    ∑ k ∈ Finset.range (p + 1), ((p + 1).choose (k + 1)) *
+      (((fwdDiffₗ R R 1 ^ k) fun y ↦ ∑ i ∈ Finset.range (n + 1), a i * y ^ i) 0) := by
+    have sum_choose_eq_choose_succ_succ :


This intermediate result is docs#Nat.sum_Icc_choose

AntoineChambert-Loir · 2025-07-10T22:32:51Z

Mathlib/Algebra/Group/ForwardDiff.lean

+      mul_one, zsmul_eq_mul, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_one,
+      Int.cast_natCast]
+
+/--


Faulhaber's formula exists in mathlib, as docs#sum_range_pow but your formula does not involve Bernoulli numbers, so the relation is not explicit.

AntoineChambert-Loir · 2025-07-10T22:33:19Z

Mathlib/Algebra/Group/ForwardDiff.lean

+A formula for the sum of a polynomial sequence `∑_{i=0..p} P(i)`, which
+generalizes **Faulhaber's formula**.
+-/
+theorem sum_of_poly_sequence {p n : ℕ} (a : ℕ → R) :


I'd guess this should be a formula for polynomials (and not sequences of coefficients).

In the formula below, I would pay attention to the name of indices: keeping a k all the way out. This will make apparent that your formula is really the combination of simpler formulas for monomials $$i \mapsto i^k$$.
0r maybe, you can just replace ∑ k ∈ Finset.range (n + 1), a k * i ^ k with a polynomial P.

In the formula below, I would pay attention to the name of indices: keeping a k all the way out. This will make apparent that your formula is really the combination of simpler formulas for monomials i ↦ i k . 0r maybe, you can just replace ∑ k ∈ Finset.range (n + 1), a k * i ^ k with a polynomial P.

We're not very experienced in representing polynomials. May you give us a specific demo? We'll adjust our code based on the example.

Ruben-VandeVelde

Some stylistic comments below, thanks

Ruben-VandeVelde · 2025-07-11T08:16:06Z

Mathlib/Algebra/Group/ForwardDiff.lean

+  exact Finset.sum_congr rfl fun k hk ↦ have _ := Finset.mem_range.1 hk; by
+    congr 1


Suggested change

exact Finset.sum_congr rfl fun k hk ↦ have _ := Finset.mem_range.1 hk; by

congr 1

exact Finset.sum_congr rfl fun k hk ↦ by

have _ := Finset.mem_range.1 hk

congr 1

Similar changes needed elsewhere

Ruben-VandeVelde · 2025-07-11T08:16:56Z

Mathlib/Algebra/Group/ForwardDiff.lean

+differences at `0`, weighted by binomial coefficients.
+`f(x) = ∑_{k=0..p} (p choose k) * (Δ^k f)(0)`.
+-/
+theorem fwdDiffTab_0th_diag_poly' {n p : ℕ} (a : ℕ → R):


I'm not seeing anything called fwdDiffTab in the signature, so this probably needs another name. Also add a space before the final :

Ruben-VandeVelde · 2025-07-11T08:17:27Z

Mathlib/Algebra/Group/ForwardDiff.lean

+-/
+theorem fwdDiff_iter_pow_eq_zero_of_lt {j n : ℕ} (h : j < n) :
+  ((fwdDiffₗ R R 1 ^ n) fun x ↦ x ^ j) = 0 := by
+  induction' n with n ih generalizing j


Please use unprimed induction in new code

Ruben-VandeVelde · 2025-07-11T08:17:40Z

Mathlib/Algebra/Group/ForwardDiff.lean

+degree `p` is zero.
+-/
+theorem fwdDiff_iter_pow_eq_zero_of_lt {j n : ℕ} (h : j < n) :
+  ((fwdDiffₗ R R 1 ^ n) fun x ↦ x ^ j) = 0 := by


The signature is indented 4 spaces

Suggested change

((fwdDiffₗ R R 1 ^ n) fun x ↦ x ^ j) = 0 := by

((fwdDiffₗ R R 1 ^ n) fun x ↦ x ^ j) = 0 := by

Ruben-VandeVelde · 2025-07-11T08:18:38Z

Mathlib/Algebra/Group/ForwardDiff.lean

+  ((fwdDiffₗ R R 1 ^ n) fun x ↦ x ^ n) = (fun _ ↦ (n.factorial : R))  := by
+  induction' n with n ih
+  · simp only [pow_zero, Module.End.one_apply, factorial_zero, cast_one]
+  · simp at ih


This needs squeezing

Ruben-VandeVelde · 2025-07-11T08:18:53Z

Mathlib/Algebra/Group/ForwardDiff.lean

+      ext x;
+      simp only [fwdDiffₗ_apply, nsmul_eq_mul, sum_apply, Pi.mul_apply, Pi.natCast_apply,
+        fwdDiff, add_pow, one_pow, Finset.sum_range_succ, Nat.choose_self, cast_one, mul_one,
+        add_sub_assoc, sub_self, add_zero, ]


Suggested change

add_sub_assoc, sub_self, add_zero, ]

add_sub_assoc, sub_self, add_zero]

Ruben-VandeVelde · 2025-07-11T08:19:15Z

Mathlib/Algebra/Group/ForwardDiff.lean

+    simp; ext x
+    simp only [Pi.zero_apply]
+  · rw [pow_succ, Module.End.mul_apply]
+    have :((fwdDiffₗ R R 1 ^ (n + 1)) (fun x => ∑ k ∈ range (n + 1), a k * x ^ k)) =


Suggested change

have :((fwdDiffₗ R R 1 ^ (n + 1)) (fun x => ∑ k ∈ range (n + 1), a k * x ^ k)) =

have : ((fwdDiffₗ R R 1 ^ (n + 1)) (fun x => ∑ k ∈ range (n + 1), a k * x ^ k)) =

Ruben-VandeVelde · 2025-07-11T08:19:47Z

Mathlib/Algebra/Group/ForwardDiff.lean

+        (∑ k ∈ range (n + 1), fun x =>  a k * x ^ k) := by
+        ext x; simp only [Finset.sum_apply]
+      simp only [this, map_sum, sum_apply]
+      rfl


What's this rfl doing? Please use the relevant API

Ruben-VandeVelde · 2025-07-11T08:20:07Z

Mathlib/Algebra/Group/ForwardDiff.lean

+      ((fun x : R ↦ a k) * (fun x : R ↦  x ^ k)) := by
+      ext x; simp
+      have : (fun x => ∑ k ∈ range (n + 1), a k * x ^ k) =
+        (∑ k ∈ range (n + 1), fun x =>  a k * x ^ k) := by


Suggested change

(∑ k ∈ range (n + 1), fun x => a k * x ^ k) := by

(∑ k ∈ range (n + 1), fun x => a k * x ^ k) := by

Please review the entire PR for spacing issues

Ruben-VandeVelde · 2025-07-11T08:21:44Z

Mathlib/Algebra/Group/ForwardDiff.lean

+A formula for the sum of a polynomial sequence `∑_{i=0..p} P(i)`, which
+generalizes **Faulhaber's formula**.
+-/
+theorem sum_of_poly_sequence {p n : ℕ} (a : ℕ → R) :


This name does not seem to make sense; at least of should only be used to indicate hypotheses

FlAmmmmING added 3 commits July 6, 2025 00:09

Update Bell.lean

75dfc8b

feat(Combinatorics/Enumerative/Bell.lean): Add definitions of standrad bell number

Update Bell.lean

8761ad0

Update ForwardDiff.lean

bacc6c6

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc) labels Jul 5, 2025

FlAmmmmING added 3 commits July 6, 2025 00:47

Update ForwardDiff.lean

792ebf8

Update ForwardDiff.lean

c41717a

Update ForwardDiff.lean

3594e71

FlAmmmmING changed the title ~~feat(Algebra/Group /ForwardDiff.lea): Add five key formulae about the forward difference operator~~ feat(Algebra/Group /ForwardDiff.lean): Add five key formulae about the forward difference operator Jul 5, 2025

FlAmmmmING changed the title ~~feat(Algebra/Group /ForwardDiff.lean): Add five key formulae about the forward difference operator~~ feat(Algebra/Group /ForwardDiff.lean): add five theorems for forward difference Jul 5, 2025

madvorak approved these changes Jul 6, 2025

View reviewed changes

madvorak reviewed Jul 6, 2025

View reviewed changes

jasin added 4 commits July 7, 2025 15:34

Update 1 fwdDiff.lean

db0b89b

Update 2 fwdDiff.lean

b064f14

Update 3 fwdDiff.lean

79cc69b

Update fwdDiff.lean

f468c95

kckennylau reviewed Jul 7, 2025

View reviewed changes

jasin added 2 commits July 9, 2025 17:06

Update fwdDiff.lean

d57edfb

Update fwdDiff.lean

37acc8a

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Jul 9, 2025

jasin added 2 commits July 9, 2025 18:42

Update remark in fwdDiff.lean

3a6f53b

Simpfiy the proof in fwdDiff.lean

d9ab68b

AntoineChambert-Loir reviewed Jul 10, 2025

View reviewed changes

Ruben-VandeVelde reviewed Jul 11, 2025

View reviewed changes

jasin added 3 commits July 11, 2025 21:46

Simpfiy the proof in fwdDiff.lean(without rename the theorem)

cf17e04

Reformat the code in fwdDiff.lean

b6b65b6

Reformat the code in fwdDiff.lean

6bbcb31

	Δ_[1] ^[n] (fun x ↦ x ^ j : ℕ → R) x = (fun _ ↦ 0) x := by
	Δ_[1] ^[n] (fun x ↦ x ^ j : ℕ → R) x = (fun _ ↦ 0) x := by

	conv_lhs=> enter[2]; ext k; enter[2]; rw [fwdDiff, ← Nat.cast_pow,
	conv_lhs => enter[2]; ext k; enter[2]; rw [fwdDiff, ← Nat.cast_pow,

	Δ_[1] ^[n] (fun x ↦ x ^ n : ℕ → R) x = (fun _ ↦ n.factorial) x := by
	Δ_[1] ^[n] (fun x ↦ x ^ n : ℕ → R) x = (fun _ ↦ n.factorial) x := by

	conv_lhs=> enter[2];ext k;enter[2,1,1]; rw [add_pow, Finset.sum_range_succ]
	conv_lhs => enter[2];ext k;enter[2,1,1]; rw [add_pow, Finset.sum_range_succ]

	conv_lhs=> enter[2]; ext k; enter[2, 1]; rw [Nat.add_sub_cancel_right]
	conv_lhs => enter[2]; ext k; enter[2, 1]; rw [Nat.add_sub_cancel_right]

	conv_lhs=> enter [2]; ext k; rw [mul_assoc, ← Nat.cast_mul, Finset.mul_sum]
	conv_lhs => enter [2]; ext k; rw [mul_assoc, ← Nat.cast_mul, Finset.mul_sum]

	(∑ k ∈ Finset.range (n + 1), a k • (x ^ k) : R[X]) =
	(∑ k ∈ Finset.range (n + 1), a k • (x ^ k) : R[X]) =

		exact Finset.sum_congr rfl fun k hk ↦ have _ := Finset.mem_range.1 hk; by
		congr 1

	((fwdDiffₗ R R 1 ^ n) fun x ↦ x ^ j) = 0 := by
	((fwdDiffₗ R R 1 ^ n) fun x ↦ x ^ j) = 0 := by

	add_sub_assoc, sub_self, add_zero, ]
	add_sub_assoc, sub_self, add_zero]

	have :((fwdDiffₗ R R 1 ^ (n + 1)) (fun x => ∑ k ∈ range (n + 1), a k * x ^ k)) =
	have : ((fwdDiffₗ R R 1 ^ (n + 1)) (fun x => ∑ k ∈ range (n + 1), a k * x ^ k)) =

	(∑ k ∈ range (n + 1), fun x => a k * x ^ k) := by
	(∑ k ∈ range (n + 1), fun x => a k * x ^ k) := by

feat(Algebra/Group /ForwardDiff.lean): add five theorems for forward difference #26793

Are you sure you want to change the base?

feat(Algebra/Group /ForwardDiff.lean): add five theorems for forward difference #26793

Conversation

FlAmmmmING commented Jul 5, 2025

Uh oh!

github-actions bot commented Jul 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 063d2e5dac

Import changes for modified files

Declarations diff

Uh oh!

madvorak left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

AntoineChambert-Loir Jul 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jul 5, 2025 •

edited

Loading

AntoineChambert-Loir Jul 10, 2025 •

edited

Loading