ChineseRemainderStarter

The Chinese remainder theorem through the public number-theory import

Open in Workbench View on GitHub

1-- The Chinese remainder theorem through the public number-theory import2-- 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 ChineseRemainderStarter8import Grace.Cumulus.NumberTheory910theorem simultaneous_residues (m n a b : Integer)11  requires coprime : IntegerCoprime(m, n)12  shows ∃ x, Integer(x) ∧ IntegerCongruent(m, x, a) ∧ IntegerCongruent(n, x, b)13proof14  exact ChineseRemainder.exists at m, n, a, b with *1516theorem unique_modulo_product (m n a b x y : Integer)17  requires coprime : IntegerCoprime(m, n)18  requires xm : IntegerCongruent(m, x, a)19  requires xn : IntegerCongruent(n, x, b)20  requires ym : IntegerCongruent(m, y, a)21  requires yn : IntegerCongruent(n, y, b)22  shows IntegerCongruent(m * n, x, y)23proof24  exact ChineseRemainder.unique at m, n, a, b, x, y with *2526-- 8 has residue 2 modulo 3 and residue 3 modulo 5.27theorem eight_mod_three28  shows IntegerCongruent(integerOfNat(3), integerOfNat(8), integerOfNat(2))29proof30  have equation : 8 = 2 + 3 * 231  . compute32  exact IntegerCongruent.of_natural_difference at 3, 8, 2, 2 with *3334theorem eight_mod_five35  shows IntegerCongruent(integerOfNat(5), integerOfNat(8), integerOfNat(3))36proof37  have equation : 8 = 3 + 5 * 138  . compute39  exact IntegerCongruent.of_natural_difference at 5, 8, 3, 1 with *40