Grace/Cumulus/NumberTheory/Euler.g17

Open in Workbench Download source

Imports

ResidueLists · Nat.Subtraction

Declarations

Source

1-- Euler's theorem and Fermat's little theorem: a coprime to n satisfies2-- a^φ(n) ≡ 1 (mod n), because multiplication by a permutes the units mod n3-- and so leaves their product unchanged; for a prime p, φ(p) = p − 14-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.NumberTheory.Euler10import ResidueLists11import Nat.Subtraction1213theorem units.coprime_product (n : Nat)14  requires nonzero : n ≠ 015  shows gcd(∏ units(n), n) = 116proof17  have unitsList := units.list at n18  have all := listProduct.coprime at n, units(n) with nonzero, *19  apply all20  intros x xNat positive21  have member := units.member with positive22  exact member.right2324-- An inverse of a unit is a unit.25theorem units.inverse_coprime (a b n : Nat)26  requires nonzero : n ≠ 027  requires inverse : (a * b) % n = 128  shows gcd(b, n) = 129proof30  have gNat := gcd.natural at b, n31  have dividesB := gcd.divides_left at b, n32  have dividesN := gcd.divides_right at b, n33  obtain ⟨q, qNat, equation⟩ := mod.equation at a * b, n with nonzero34  rw inverse at equation35  have bDividesProduct : b ∣ a * b36    witness a37    ring38  have dividesProduct := divides.transitive with dividesB, bDividesProduct39  have dividesMultiple := divides.multiply_right at gcd(b, n), n, q with dividesN40  rw equation at dividesProduct41  have dividesOne := divides.add_cancel_left with dividesMultiple, dividesProduct42  exact divides.one_only with gNat, dividesOne4344-- Scaling by a unit permutes the units.45theorem units.scaled_multiplicity (a n v : Nat)46  requires aboveOne : 1 < n47  requires coprime : gcd(a, n) = 148  shows multiplicity(v, scaledList(a, n, units(n))) = multiplicity(v, units(n))49proof50  have nonzero : n ≠ 051    intro zero52    rw zero at aboveOne53    have impossible : ¬(1:N) < 0 by arith54    exact impossible with aboveOne55  have unitsList := units.list at n56  obtain ⟨b, bNat, bBelow, inverse⟩ := coprime.inverse with aboveOne, coprime57  have bCoprime := units.inverse_coprime with nonzero, inverse58  have alternatives : v < n ∨ ¬v < n by tauto59  cases alternatives with vBelow | vNotBelow60  . have residues : ∀ x, Nat(x) → 0 < multiplicity(x, units(n)) → x < n61      intros x xNat positive62      have member := units.member with positive63      exact member.left64    have key := scaledList.multiplicity at a, b, n, v, units(n) with nonzero, inverse, vBelow, *65    have reduced := key with residues66    rw reduced67    have scaledBelow := mod.less at b * v, n with nonzero68    have coprimeAlternatives : gcd(v, n) = 1 ∨ gcd(v, n) ≠ 1 by tauto69    cases coprimeAlternatives with vCoprime | vNotCoprime70    . have scaledCoprime := coprime.mul_mod with nonzero, bCoprime, vCoprime71      have left := units.multiplicity with scaledBelow, scaledCoprime72      have right := units.multiplicity with vBelow, vCoprime73      rw [left, right]74      rfl75    . have scaledNotCoprime : gcd((b * v) % n, n) ≠ 176        intro scaledCoprime77        apply vNotCoprime78        have recover : (a * ((b * v) % n)) % n = v79          have step1 := mod.mul_right at n, a, b * v with nonzero80          have rearrange : a * (b * v) = (a * b) * v by ring81          have step2 := mod.mul_left at n, a * b, v with nonzero82          have one : 1 * v = v by ring83          have self := mod.of_less with vBelow84          rw [step1, rearrange, ← step2, inverse, one, self]85          rfl86        have product := coprime.mul_mod with nonzero, coprime, scaledCoprime87        rwa recover at product88      have leftNot : ¬((b * v) % n < n ∧ gcd((b * v) % n, n) = 1)89        intro both90        exact scaledNotCoprime with both.right91      have rightNot : ¬(v < n ∧ gcd(v, n) = 1)92        intro both93        exact vNotCoprime with both.right94      have left := units.multiplicity_other with leftNot95      have right := units.multiplicity_other with rightNot96      rw [left, right]97      rfl98  . have rightNot : ¬(v < n ∧ gcd(v, n) = 1)99      intro both100      exact vNotBelow with both.left101    have right := units.multiplicity_other with rightNot102    rw right103    have scaledList2 := scaledList.list at a, n, units(n) with *104    have members := scaledList.member at a, n, units(n) with nonzero, *105    have trichotomy := Less.trichotomy at 0, multiplicity(v, scaledList(a, n, units(n)))106    rcases trichotomy with positive | zero | negative107    . exfalso108      have vNat : Nat(v) by typecheck109      have below := members with v, positive110      exact vNotBelow with below111    . symm at zero112      exact zero113    . exfalso114      have impossible : ¬multiplicity(v, scaledList(a, n, units(n))) < 0 by arith115      exact impossible with negative116117-- Euler's theorem.118theorem euler.theorem (a n : Nat)119  requires aboveOne : 1 < n120  requires coprime : gcd(a, n) = 1121  shows (a ^ totient(n)) % n = 1122proof123  have nonzero : n ≠ 0124    intro zero125    rw zero at aboveOne126    have impossible : ¬(1:N) < 0 by arith127    exact impossible with aboveOne128  have unitsList := units.list at n129  have scaledUnits := scaledList.list at a, n, units(n) with *130  have sameMultiplicity : ∀ q, Nat(q) → multiplicity(q, scaledList(a, n, units(n))) = multiplicity(q, units(n))131    intros q qNat132    exact units.scaled_multiplicity with aboveOne, coprime133  have sameProducts := listProduct.of_multiplicities at scaledList(a, n, units(n)) with *134  have sameProduct := sameProducts with units(n), unitsList, sameMultiplicity135  have productMod := scaledList.product at a, n, units(n) with nonzero, *136  rw sameProduct at productMod137  have lengthDef := totient.definition at n138  rw ← lengthDef at productMod139  have productCoprime := units.coprime_product with nonzero140  have arranged : (∏ units(n) * 1) % n = (∏ units(n) * a ^ totient(n)) % n141    have one : ∏ units(n) * 1 = ∏ units(n) by ring142    have commute : ∏ units(n) * a ^ totient(n) = a ^ totient(n) * ∏ units(n) by ring143    rwa [one, commute]144  have cancelled := coprime.mul_cancel_mod with nonzero, productCoprime, arranged145  have oneSelf := mod.of_less with aboveOne146  rw oneSelf at cancelled147  symm at cancelled148  exact cancelled149150-- Below a prime, every positive residue is a unit.151theorem prime.coprime_below (p k : Nat)152  requires prime : Prime(p)153  requires positive : 0 < k154  requires below : k < p155  shows gcd(k, p) = 1156proof157  have kNonzero : k ≠ 0158    intro zero159    rw zero at positive160    exact Less.irreflexive with *, positive161  have notDivides : ¬(p ∣ k)162    intro divides163    have le := divides.le with divides, kNonzero164    have impossible : ¬p ≤ k by arith165    exact impossible with le166  have certificate := Prime.coprime_of_not_divides with prime, notDivides167  have same := gcd.unique with certificate168  have commute := gcd.commutative at k, p169  rwa commute170171theorem unitsBelow.prime_length (p j : Nat)172  requires prime : Prime(p)173  shows j < p → length{ℕ}(unitsBelow(p, succ(j))) = j174proof175  induction j176  | zero =>177    intro below178    have aboveOne := Prime.greater_than_one at p with prime179    have zeroGcd := gcd.zero_left at p180    have notCoprime : gcd(0, p) ≠ 1181      intro one182      rw zeroGcd at one183      rw one at aboveOne184      exact Less.irreflexive at 1 with *, aboveOne185    have step := unitsBelow.succ_other at p, 0 with notCoprime186    rw [step, unitsBelow.zero]187    exact length.nil at ℕ188  | succ(i) using ih =>189    intro below190    have smaller : i < p by arith191    have previous := ih with smaller192    have positive : 0 < succ(i) by arith193    have coprime := prime.coprime_below at p, succ(i) with prime, positive, below194    have step := unitsBelow.succ_unit at p, succ(i) with coprime195    have restList := unitsBelow.list at p, succ(i)196    have expand := length.cons at ℕ, succ(i), unitsBelow(p, succ(i)) with *197    rw [step, expand, previous]198    rfl199200theorem totient.prime (p : Nat)201  requires prime : Prime(p)202  shows totient(p) = p - 1203proof204  have nonzero := Prime.nonzero with prime205  have shape := natural.zero_or_successor at p206  cases shape with zero | successor207  . exfalso208    exact nonzero with zero209  . obtain ⟨q, qNat, form⟩ := successor210    have below : q < p211      rw form212      arith213    have lengths := unitsBelow.prime_length with prime214    have value := lengths with below215    have same : totient(p) = length{ℕ}(unitsBelow(p, p))216      unfold totient217      rfl218    have inner : unitsBelow(p, p) = unitsBelow(p, succ(q))219      rw ← form220      rfl221    rw [same, inner, value, form]222    simp [sub, predecessor]223224theorem fermat.little (a p : Nat)225  requires prime : Prime(p)226  requires notDivides : ¬(p ∣ a)227  shows a ^ (p - 1) % p = 1228proof229  have aboveOne := Prime.greater_than_one with prime230  have certificate := Prime.coprime_of_not_divides with prime, notDivides231  have same := gcd.unique with certificate232  have commute := gcd.commutative at a, p233  have coprime : gcd(a, p) = 1234    rwa commute235  have totientValue := totient.prime with prime236  rw ← totientValue237  exact euler.theorem with aboveOne, coprime238