Commit 2025-12-08 16:53 ac5606c7

View on Github →

feat(Combinatorics/Enumerative/Catalan): large and small Schröder numbers (#30609)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean

deleted theorem Finset.sum_Ico_add_eq_sum_Ico_add_one

Modified Mathlib/Combinatorics/Enumerative/Catalan.lean

Modified Mathlib/Combinatorics/Enumerative/DyckWord.lean

Created Mathlib/Combinatorics/Enumerative/Schroder.lean

added theorem Nat.even_largeSchroder

added def Nat.largeSchroder

added theorem Nat.largeSchroder_one

added theorem Nat.largeSchroder_succ

added theorem Nat.largeSchroder_two

added theorem Nat.largeSchroder_zero

added def Nat.smallSchroder

added theorem Nat.smallSchroder_one

added theorem Nat.smallSchroder_succ

added theorem Nat.smallSchroder_succ_eq_largeSchroder_div_two

added theorem Nat.smallSchroder_zero

added theorem Nat.two_mul_smallSchroder_succ