Partitions with distinct even parts
TheoremCongruences modulo 24 for partitions with distinct even parts#●ready to prove
Write \(\mathrm{ped}(m)\) for the number of partitions of \(m\) in which the even parts are distinct (odd parts may repeat). For every natural number \(n\), each of \(\mathrm{ped}(225n+43)\), \(\mathrm{ped}(225n+88)\), \(\mathrm{ped}(225n+133)\) and \(\mathrm{ped}(225n+223)\) is congruent to \(0\) modulo \(24\).
public theorem_wanted partitionsEvenPartsDistinct_mod24_progressions (n : ℕ) :
Nat.ModEq 24 (distinctEvenPartsCount (225 * n + 43)) 0 ∧
Nat.ModEq 24 (distinctEvenPartsCount (225 * n + 88)) 0 ∧
Nat.ModEq 24 (distinctEvenPartsCount (225 * n + 133)) 0 ∧
Nat.ModEq 24 (distinctEvenPartsCount (225 * n + 223)) 0
public def distinctEvenPartsCount (n : ℕ) : ℕ :=
((Finset.univ : Finset n.Partition).filter
fun p => ∀ i ∈ p.parts, Even i → p.parts.count i = 1).card
WantedExt/Combinatorics/Enumerative/OverpartitionsOddPartsWanted.lean:115
Sources
- Hemjyoti Nath, New Congruences for Partitions Where the Even Parts Are Distinct, INTEGERS 24 (2024), Article A79, Theorem 1.1.
Uses 1
TheoremPower-of-five congruence modulo 24 for partitions with distinct even parts#●ready to prove
Write \(\mathrm{ped}(m)\) for the number of partitions of \(m\) in which the even parts are distinct (odd parts may repeat). For all natural numbers \(k \ge 1\) and \(n\),
The quotient is exact, since \(57 \cdot 5^{2k} - 1\) is divisible by \(8\).
public theorem_wanted partitionsEvenPartsDistinct_mod24_five_power
(k n : ℕ) (hk : 1 ≤ k) :
Nat.ModEq 24 (distinctEvenPartsCount (9 * n + 7))
(distinctEvenPartsCount
(9 * 5 ^ (2 * k) * n + (57 * 5 ^ (2 * k) - 1) / 8))
public def distinctEvenPartsCount (n : ℕ) : ℕ :=
((Finset.univ : Finset n.Partition).filter
fun p => ∀ i ∈ p.parts, Even i → p.parts.count i = 1).card
WantedExt/Combinatorics/Enumerative/OverpartitionsOddPartsWanted.lean:115
Sources
- Hemjyoti Nath, New Congruences for Partitions Where the Even Parts Are Distinct, INTEGERS 24 (2024), Article A79, Theorem 1.1.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.