Grace/Cumulus/NumberTheory/CoprimeCancel.g17

Open in Workbench Download source

Imports

Modular · Coprime · Factorization

Declarations

Source

1-- Coprime factors cancel: if n is coprime to a then n divides a·t only when2-- it divides t, so multiplication by a is injective on residues mod n; a3-- product of numbers coprime to n is coprime to n, and reducing mod n keeps4-- the greatest common divisor with n5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.NumberTheory.CoprimeCancel11import Modular12import Coprime13import Factorization1415theorem coprime.cancel (a n t : Nat)16  requires coprime : gcd(a, n) = 117  requires divides : n ∣ a * t18  shows n ∣ t19proof20  have integerCoprime : IntegerCoprime(integerOfNat(n), integerOfNat(a))21    unfold IntegerCoprime22    have same := integerGCD.ofNat at n, a23    have commute := gcd.commutative at n, a24    rwa [same, commute]25  have product := integerOfNat.mul at a, t26  have magnitude := integerNatAbs.ofNat at a * t27  have bridge := IntegerDivides.natural_left at n, integerOfNat(a * t)28  have integerDivides : IntegerDivides(integerOfNat(n), integerOfNat(a) * integerOfNat(t))29    rw ← product30    apply bridge.backward31    rwa magnitude32  have cancelled := IntegerCoprime.cancel with integerCoprime, integerDivides33  have back := IntegerDivides.natural_left at n, integerOfNat(t)34  have result := back.forward with cancelled35  have magnitudeT := integerNatAbs.ofNat at t36  rwa magnitudeT at result3738-- Multiplication by a coprime factor is injective on remainders.39theorem coprime.mul_cancel_mod_le (a n x y : Nat)40  requires nonzero : n ≠ 041  requires coprime : gcd(a, n) = 142  requires below : x ≤ y43  requires same : (a * x) % n = (a * y) % n44  shows x % n = y % n45proof46  obtain ⟨t, tNat, shape⟩ := below47  rw ← shape at same48  have expand : a * (x + t) = a * x + a * t by ring49  rw expand at same50  symm at same51  have dividesProduct := mod.add_cancel with nonzero, same52  obtain ⟨s, sNat, form⟩ := coprime.cancel at a, n, t with coprime, dividesProduct53  rw [← shape, ← form]54  have shifted := mod.add_multiple at n, x, s with nonzero55  symm at shifted56  exact shifted5758theorem coprime.mul_cancel_mod (a n x y : Nat)59  requires nonzero : n ≠ 060  requires coprime : gcd(a, n) = 161  requires same : (a * x) % n = (a * y) % n62  shows x % n = y % n63proof64  have total := LessEqual.total at x, y65  cases total with below | above66  . exact coprime.mul_cancel_mod_le with nonzero, coprime, below, same67  . symm at same68    have flipped := coprime.mul_cancel_mod_le with nonzero, coprime, above, same69    symm at flipped70    exact flipped7172-- Reducing mod n does not change the greatest common divisor with n.73theorem coprime.mod (a n : Nat)74  requires nonzero : n ≠ 075  shows gcd(a % n, n) = gcd(a, n)76proof77  have first := gcd.euclidean at a, n with nonzero78  have second := gcd.euclidean at a % n, n with nonzero79  have idempotent := mod.mod at n, a with nonzero80  rw [second, idempotent, first]81  rfl8283-- A product of numbers coprime to n is coprime to n.84theorem coprime.mul (a b n : Nat)85  requires nonzero : n ≠ 086  requires coprimeA : gcd(a, n) = 187  requires coprimeB : gcd(b, n) = 188  shows gcd(a * b, n) = 189proof90  have gNat := gcd.natural at a * b, n91  have dividesN := gcd.divides_right at a * b, n92  have dividesProduct := gcd.divides_left at a * b, n93  have gNonzero : gcd(a * b, n) ≠ 094    intro zero95    rw zero at dividesN96    have nZero := zero.divides_only_zero with dividesN97    exact nonzero with nZero98  have trichotomy := Less.trichotomy at 1, gcd(a * b, n)99  rcases trichotomy with above | equal | below100  . exfalso101    obtain ⟨p, prime, dividesG⟩ := natural.exists_prime_divisor with above102    have pNat := Prime.natural with prime103    have pDividesProduct := divides.transitive with dividesG, dividesProduct104    have pDividesN := divides.transitive with dividesG, dividesN105    have pAboveOne := Prime.greater_than_one with prime106    have split := Prime.divides_mul with prime, pDividesProduct107    cases split with dividesA | dividesB108    . have dividesGcd := gcd.greatest with dividesA, pDividesN109      rw coprimeA at dividesGcd110      have pOne := divides.one_only with pNat, dividesGcd111      rw pOne at pAboveOne112      exact Less.irreflexive with *, pAboveOne113    . have dividesGcd := gcd.greatest with dividesB, pDividesN114      rw coprimeB at dividesGcd115      have pOne := divides.one_only with pNat, dividesGcd116      rw pOne at pAboveOne117      exact Less.irreflexive with *, pAboveOne118  . symm at equal119    exact equal120  . exfalso121    have atMostZero := Less.successor_upper at gcd(a * b, n), 0 with below122    have zeroLe := Grace.Cumulus.Nat.Order.LessEqual.zero at gcd(a * b, n)123    have zero := LessEqual.antisymmetric with atMostZero, zeroLe124    exact gNonzero with zero125126theorem coprime.mul_mod (a b n : Nat)127  requires nonzero : n ≠ 0128  requires coprimeA : gcd(a, n) = 1129  requires coprimeB : gcd(b, n) = 1130  shows gcd((a * b) % n, n) = 1131proof132  have reduce := coprime.mod at a * b, n with nonzero133  rw reduce134  exact coprime.mul with nonzero, coprimeA, coprimeB135