ArithmeticResidueReversal.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Agreement of the residue split with integer reversal

theorem OAI.Ostmann.intCast_frequency_zero_iff line 9
theorem OAI.Ostmann.ArithmeticResidueSplit.numerator_integer line 13
theorem OAI.Ostmann.ArithmeticResidueSplit.frequency_test_integer line 26
Source documentation
The frequency-divisibility test in the residue evaluator is precisely the integer test, including either sign of the frequency.
```
theorem ArithmeticResidueSplit.frequency_test_integer {Q : ℕ}
    (d : ArithmeticResidueSplit Q) (x : (ZMod Q)ˣ) (N : ℤ)
    (hN : d.numerator x = N) :
    d.reduce (d.numerator x) = 0 ↔ d.frequencies.root ∣ N := by
…
```
Mentions: OAI.Ostmann.ArithmeticResidueSplit
def OAI.Ostmann.ArithmeticResidueSplit.pivot line 33

theorem OAI.Ostmann.ArithmeticResidueSplit.pivot_integer line 40

Source documentation

The residue evaluator reconstructs the same pivot as the original integer formula, at the remaining precision.

theorem ArithmeticResidueSplit.pivot_integer {R M : ℕ} [NeZero M]
    (d : ArithmeticResidueSplit (R * M)) (hsR : d.frequencies.root.natAbs ∣ R)
    (U : (ZMod M)ˣ) (x : (ZMod (R * M))ˣ) (u p : ℤ)
    (hU : (U : ZMod M) = u)
    (hN : d.numerator x = (d.frequencies.root * u * p : ℤ)) :
    d.pivot hsR U x = p := by
…

Mentions: OAI.Ostmann.ArithmeticResidueSplit