ResidueDigitsContract.lean

1 module
2 public import ResidueLiftDigits
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace Komorebi.ResidueDigitsContract
8 
9 /-- The target contains actual next-level residue vectors retaining the lower
10 residue, not arbitrary integer representatives or all next-level roots. -/
11 def explicit_residue_digit_equivalence (q L : ℕ) (hq : 0 < q) {d : ℕ}
12     (x : Fin d → ℤ) :
13     (Fin d → ZMod q) ≃
14       {y : Fin d → ZMod (q^(L+1)) //
15         ∀ i, (q : ℤ)^L ∣ ((y i).val : ℤ) - x i} :=
16   ResidueLiftDigits.digitEquivResidue q L hq x
17 
18 /-- The forward map is exactly the prescribed digit shift. -/
19 theorem explicit_residue_digit_formula (q L : ℕ) (hq : 0 < q) {d : ℕ}
20     (x : Fin d → ℤ) (t : Fin d → ZMod q) (i : Fin d) :
21     (explicit_residue_digit_equivalence q L hq x t).val i =
22       ((x i + (q : ℤ)^L * ((t i).val : ℤ) : ℤ) : ZMod (q^(L+1))) := rfl
23 
24 end Komorebi.ResidueDigitsContract

Back to source controls