Grace/Cumulus/Algebra/Group/PrimeBinomial.g17

Open in Workbench Download source

Imports

Combinatorics.Vandermonde · NumberTheory.Factorization · NumberTheory.Modular

Declarations

Source

1-- Binomial coefficients at a prime power: p does not divide2-- (p^k·m choose p^k) when p does not divide m3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.Group.PrimeBinomial9import Combinatorics.Vandermonde10import NumberTheory.Factorization11import NumberTheory.Modular1213-- The inner entries of row p of Pascal's triangle are divisible by p.14theorem choose.prime_middle (p j : Nat)15  requires prime : Prime(p)16  requires positive : 0 < j17  requires below : j < p18  shows p ∣ p choose j19proof20  obtain ⟨i, iNat, jShape⟩ := Less.exists_add_one with positive21  obtain ⟨n, nNat, pShape⟩ := Less.exists_add_one with below22  have zeroAdd : 0 + i + 1 = i + 1 by ring23  rw zeroAdd at jShape24  have absorbed := choose.absorption_at at j + n, i25  have rowShape : j + n + 1 = p26    rw pShape27    ring28  have row : (i + 1) * (p choose (i + 1)) = p * ((j + n) choose i)29    rw ← rowShape30    exact absorbed31  rw ← jShape at row32  have cNat := choose.natural at j + n, i33  have product : p ∣ j * (p choose j)34    witness (j + n) choose i35    rw row36    rfl37  have split := Prime.divides_mul with prime, product38  cases split with dividesJ | dividesEntry39  . exfalso40    have jNonzero : j ≠ 041      intro zero42      rw zero at positive43      exact Less.irreflexive at 0 with positive44    have bound := divides.le with dividesJ, jNonzero45    have strict := LessEqual.transitive_Less with bound, below46    exact Less.irreflexive with strict47  . exact dividesEntry4849-- Modulo p, the first t ≤ p terms of the convolution with row p reduce to50-- the term i = 0.51theorem chooseConvolution.mod_prime (p n r t : Nat)52  requires prime : Prime(p)53  requires below : t < p54  shows chooseConvolution(p, n, r, t + 1) % p = (n choose r) % p55proof56  induction t57  | zero =>58    intro below59    have one : 0 + 1 = 1 by compute60    rw [one, chooseConvolution.one]61    rfl62  | k + 1 using ih =>63    intro below64    have pNonzero := Prime.nonzero with prime65    have earlier : k < p by arith66    have reduced := ih with earlier67    have positive : 0 < k + 1 by arith68    obtain ⟨s, sNat, entry⟩ :=69      choose.prime_middle with prime, positive, below70    have cNat := choose.natural at n, r - (k + 1)71    have split := chooseConvolution.succ at p, n, r, k + 172    have multiple : (p choose (k + 1)) * (n choose (r - (k + 1))) =73        p * (s * (n choose (r - (k + 1))))74      rw ← entry75      ring76    rw [split, multiple, mod.add_multiple]77    exact reduced7879-- Beyond the row, the convolution with row p gains nothing.80theorem chooseConvolution.beyond_row (p n r d : Nat)81  shows chooseConvolution(p, n, r, p + 1 + d) =82    chooseConvolution(p, n, r, p + 1)83proof84  induction d85  | zero =>86    have shape : p + 1 + 0 = p + 1 by ring87    rw shape88    rfl89  | k + 1 using ih =>90    have shape : p + 1 + (k + 1) = p + 1 + k + 1 by ring91    have below : p < p + 1 + k by arith92    have vanishes := choose.above_diagonal with below93    have cNat := choose.natural at n, r - (p + 1 + k)94    rw [shape, chooseConvolution.succ, vanishes, ih]95    ring9697-- One step of Lucas' theorem: modulo p, (p + n) choose r is the sum of two98-- entries of row n, p apart.99theorem choose.prime_add_mod (p n r : Nat)100  requires prime : Prime(p)101  requires le : p ≤ r102  shows ((p + n) choose r) % p = ((n choose r) + (n choose (r - p))) % p103proof104  have pNonzero := Prime.nonzero with prime105  obtain ⟨d, dNat, rShape⟩ := le106  have positive := Less.positive_of_ne_zero with pNonzero107  obtain ⟨q, qNat, pShape⟩ := Less.exists_add_one with positive108  have zeroAdd : 0 + q + 1 = q + 1 by ring109  rw zeroAdd at pShape110  have rowShape : r + 1 = p + 1 + d111    rw ← rShape112    ring113  have full := choose.vandermonde_at at p, n, r114  have beyond := chooseConvolution.beyond_row at p, n, r, d115  have top := chooseConvolution.succ at p, n, r, p116  have last := choose.diagonal at p117  have inner : chooseConvolution(p, n, r, q + 1) % p = (n choose r) % p118    have below : q < p by arith119    exact chooseConvolution.mod_prime with prime, below120  rw ← pShape at inner121  have cNat := choose.natural at n, r - p122  have convNat := chooseConvolution.natural at p, n, r, p123  have entryNat := choose.natural at n, r124  have topValue : chooseConvolution(p, n, r, p + 1) =125      chooseConvolution(p, n, r, p) + (n choose (r - p))126    rw [top, last]127    ring128  have back := mod.add at p, n choose r, n choose (r - p) with pNonzero129  calc130    ((p + n) choose r) % p = chooseConvolution(p, n, r, r + 1) % p := by rw full131    _ = chooseConvolution(p, n, r, p + 1) % p := by rw [rowShape, beyond]132    _ = (chooseConvolution(p, n, r, p) + (n choose (r - p))) % p :=133      by rw topValue134    _ = (chooseConvolution(p, n, r, p) % p + (n choose (r - p)) % p) % p :=135      mod.add with pNonzero136    _ = ((n choose r) % p + (n choose (r - p)) % p) % p := by rw inner137    _ = ((n choose r) + (n choose (r - p))) % p := by rw ← back138139-- Lucas' theorem in one digit: (p·a choose p·b) ≡ (a choose b) modulo p.140theorem choose.mul_prime_mod (p a : Nat)141  requires prime : Prime(p)142  shows ∀ b, Nat(b) → ((p * a) choose (p * b)) % p = (a choose b) % p143proof144  induction a145  | zero =>146    intros b bNat147    have pPositive := Less.positive_of_ne_zero with (Prime.nonzero with prime)148    have zero : p * 0 = 0 by ring149    rw zero150    have split := natural.zero_or_successor at b151    cases split with isZero | isSucc152    . rw [isZero, zero]153      rfl154    . obtain ⟨j, jNat, shape⟩ := isSucc155      have jBelow : 0 < succ(j) by arith156      have below := Less.mul_positive with pPositive, jBelow157      rw [shape, choose.above_diagonal, choose.above_diagonal]158      rfl159  | k + 1 using ih =>160    intros b bNat161    have pNonzero := Prime.nonzero with prime162    have split := natural.zero_or_successor at b163    cases split with isZero | isSucc164    . have zero : p * 0 = 0 by ring165      rw [isZero, zero, choose.zero_right, choose.zero_right]166      rfl167    . obtain ⟨j, jNat, shape⟩ := isSucc168      have hj : j + 1 = succ(j) := add.right_one at j169      rw [shape, ← hj]170      have rowShape : p * (k + 1) = p + p * k by ring171      have columnShape : p * (j + 1) = p * j + p by ring172      have multipleNat : Nat(p * j) by typecheck173      have le : p ≤ p * j + p by arith174      have step := choose.prime_add_mod at p, p * k, p * j + p with prime, le175      have cancel := sub.add_right at p * j, p176      have first := ih with j + 1, assumption177      have second := ih with j, jNat178      rw columnShape at first179      have pascal := choose.pascal at k, j180      have leftNat := choose.natural at p * k, p * j + p181      have rightNat := choose.natural at p * k, p * j182      have aNat := choose.natural at k, j183      have bNat2 := choose.natural at k, j + 1184      have back := mod.add at p, k choose (j + 1), k choose j with pNonzero185      have swapped : (k + 1) choose (j + 1) = (k choose (j + 1)) + (k choose j)186        rw pascal187        ring188      rw cancel at step189      have reshaped : ((p * (k + 1)) choose (p * (j + 1))) % p =190          ((p + p * k) choose (p * j + p)) % p191        rw [rowShape, columnShape]192        rfl193      have expanded := mod.add at p, (p * k) choose (p * j + p),194        (p * k) choose (p * j) with pNonzero195      rw [reshaped, step, expanded, first, second, ← back, swapped]196      rfl197198-- Iterating down the powers of p: (p^k·m choose p^k) ≡ m modulo p.199theorem choose.prime_power_mod (p m k : Nat)200  requires prime : Prime(p)201  shows ((p ^ k * m) choose (p ^ k)) % p = m % p202proof203  induction k204  | zero =>205    have one : p ^ 0 * m = m206      rw pow.zero207      ring208    rw [one, pow.zero, choose.one_right]209    rfl210  | j + 1 using ih =>211    have powNat := pow.closed at p, j212    have row : p ^ (j + 1) * m = p * (p ^ j * m)213      rw pow.add_one214      ring215    have column : p ^ (j + 1) = p * p ^ j := pow.add_one at p, j216    have step := choose.mul_prime_mod at p, p ^ j * m with prime217    have reduced := step with p ^ j, powNat218    rw [row, column, reduced]219    exact ih220221-- The binomial coefficient of Wielandt's argument is not divisible by p.222theorem choose.prime_power_not_divides (p k m : Nat)223  requires prime : Prime(p)224  requires notDivides : ¬(p ∣ m)225  shows ¬(p ∣ (p ^ k * m) choose (p ^ k))226proof227  intro divides228  have pNonzero := Prime.nonzero with prime229  have reduced := choose.prime_power_mod at p, m, k with prime230  have vanishes := mod.zero_iff.backward with pNonzero, divides231  rw reduced at vanishes232  have dividesM := mod.zero_iff.forward with pNonzero, vanishes233  exact notDivides with dividesM234