4.7. Using the theorems with Mathlib
Mathlib defines a ≡ b [ZMOD n] to mean a % n = b % n, so the congruence
theorems of this library are already statements about Int.ModEq:
example {c c' : Crt} {r : Int} {m : Nat}
(h : c.push r m = some c') :
c'.value ≡ r [ZMOD m] :=
Crt.push_congr_new h
The theorems about reconstruction translate to ZMod m. By
ratRecon?_den_coprime, the denominator of the fraction found by ratRecon?
is a unit in ZMod m, and the image of the fraction there is the residue it
was reconstructed from:
example {a P Q : Int} {m : Nat} {x : Rat}
(h : ratRecon? a m P Q = some x) :
(x.num : ZMod m) * (x.den : ZMod m)⁻¹ = a := a:ℤP:ℤQ:ℤm:ℕx:Rath:ratRecon? a m P Q = some x⊢ ↑x.num * (↑x.den)⁻¹ = ↑a
a:ℤP:ℤQ:ℤm:ℕx:Rath:ratRecon? a m P Q = some xhd:↑m ∣ ↑x.den * a - x.num⊢ ↑x.num * (↑x.den)⁻¹ = ↑a
a:ℤP:ℤQ:ℤm:ℕx:Rath:ratRecon? a m P Q = some xhd:↑m ∣ ↑x.den * a - x.numkey:↑x.num = ↑(↑x.den * a)⊢ ↑x.num * (↑x.den)⁻¹ = ↑a
a:ℤP:ℤQ:ℤm:ℕx:Rath:ratRecon? a m P Q = some xhd:↑m ∣ ↑x.den * a - x.numkey:↑x.num = ↑x.den * ↑a⊢ ↑x.num * (↑x.den)⁻¹ = ↑a
All goals completed! 🐙
end HexModularChapter