Grace/Cumulus/NumberTheory/ModularInverse.g17

Open in Workbench Download source

Imports

CoprimeCancel · Cardinal

Declarations

Source

1-- Every residue coprime to n has a multiplicative inverse mod n: scaling the2-- residues below n by a is injective, so by counting it is onto, and some3-- residue is sent to one4-- 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.ModularInverse10import CoprimeCancel11import Cardinal1213-- Multiplication by a on the residues below n.14defgraph scaleMod (a n : Nat) (x ∈ n) : n := mod(mul(a, x), n)15requires nonzero : n ≠ 016proof17  have xNat := natural.member at n with member18  have bound := mod.less at a * x, n with nonzero19  exact membership.of_Less at (a * x) % n, n with *, *, bound2021theorem scaleMod.injective (a n : Nat)22  requires nonzero : n ≠ 023  requires coprime : gcd(a, n) = 124  shows InjectiveBetween(scaleMod(a, n), n, n)25proof26  have function := scaleMod.function at a, n with nonzero27  constructor28  . exact function29  . intros x hx y hy z hz hxz hyz30    have xValue := FunctionBetween.apply_value with function, hx, hxz31    have yValue := FunctionBetween.apply_value with function, hy, hyz32    have xScaled := scaleMod.value at a, n, x with *33    have yScaled := scaleMod.value at a, n, y with *34    have xNat := natural.member at n with hx35    have yNat := natural.member at n with hy36    have same : (a * x) % n = (a * y) % n37      rw [← xScaled, ← yScaled, xValue, yValue]38      rfl39    have residues := coprime.mul_cancel_mod with nonzero, coprime, same40    have xBelow := Less.of_membership with hx41    have yBelow := Less.of_membership with hy42    have xSelf := mod.of_less with xBelow43    have ySelf := mod.of_less with yBelow44    rwa [xSelf, ySelf] at residues4546theorem scaleMod.onto (a n : Nat)47  requires nonzero : n ≠ 048  requires coprime : gcd(a, n) = 149  shows functionImage(scaleMod(a, n), n, n) = n50proof51  have injective := scaleMod.injective with nonzero, coprime52  have finite := Finite.natural at n53  have subset : functionImage(scaleMod(a, n), n, n) ⊆ n54    intros y hy55    have parts := functionImage.membership.forward with hy56    exact parts.left57  have reflexive : n ⊆ n58    intros y hy59    exact hy60  have same := cardinality.injective_image with injective, reflexive, finite61  exact cardinality.eq_subset with finite, subset, same6263theorem coprime.inverse (a n : Nat)64  requires aboveOne : 1 < n65  requires coprime : gcd(a, n) = 166  shows ∃ b, Nat(b) ∧ b < n ∧ (a * b) % n = 167proof68  have nonzero : n ≠ 069    intro zero70    rw zero at aboveOne71    have impossible : ¬(1:N) < 0 by arith72    exact impossible with aboveOne73  have onto := scaleMod.onto with nonzero, coprime74  have oneIn : (1:N) ∈ n by exact membership.of_Less at (1:N), n with *, *, aboveOne75  rw ← onto at oneIn76  have parts := functionImage.membership.forward with oneIn77  obtain ⟨b, hb, equation⟩ := parts.right78  have bNat := natural.member at n with hb79  have value := scaleMod.value at a, n, b with *80  witness b81  constructor82  . exact Less.of_membership with hb83  . rw [value] at equation84    symm at equation85    exact equation86