CoprimeStarter

Coprime cancellation and modular inverse examples

Open in Workbench View on GitHub

1-- Coprime cancellation and modular inverse examples2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module CoprimeStarter8import Grace.Cumulus.NumberTheory910theorem cancel_coprime_factor (a b c : Integer)11  requires coprime : IntegerCoprime(a, b)12  requires product : IntegerDivides(a, b * c)13  shows IntegerDivides(a, c)14proof15  exact IntegerCoprime.cancel at a, b, c with *1617theorem inverse_exists (a m : Integer)18  requires coprime : IntegerCoprime(a, m)19  shows ∃ u, Integer(u) ∧ IntegerCongruent(m, a * u, integerOne)20proof21  exact IntegerCoprime.modular_inverse at a, m with *2223theorem inverse_unique_modulo (a m u v : Integer)24  requires first : IntegerCongruent(m, a * u, integerOne)25  requires second : IntegerCongruent(m, a * v, integerOne)26  shows IntegerCongruent(m, u, v)27proof28  exact IntegerCongruent.inverse_unique at m, a, u, v with *2930-- 4 is an inverse of 3 modulo 11, certified from 12 = 1 + 11*1.31theorem inverse_three_mod_eleven32  shows IntegerCongruent(integerOfNat(11), integerOfNat(3) * integerOfNat(4), integerOne)33proof34  have difference : 12 = 1 + 11 * 135  . compute36  have congruent := IntegerCongruent.of_natural_difference at 11, 12, 1, 1 with *37  have product := integerOfNat.mul at 3, 4 with *38  have twelve : 3 * 4 = 1239  . compute40  rw twelve at product41  rw product at congruent42  simpa [integerOne] using congruent43