PivotKeyReduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Reduction of the actual integer pivot key at each constituent prime

theorem OAI.Ostmann.pivotResidueKey_val line 11

theorem OAI.Ostmann.pivotResidueKey_mul line 20

Source documentation

Key multiplication is valid already modulo the complete composite pivot.

theorem pivotResidueKey_mul (M : ℕ) [NeZero M] (L : ℕ) (v : ℤ)
    (hL : L.Coprime M) :
    ((pivotResidueKey M L v).val : ZMod M) * (L : ZMod M) = (v : ZMod M) := by
…

Mentions: OAI.Ostmann.pivotResidueKey

theorem OAI.Ostmann.pivotResidueKey_mul_at_divisor line 28
Source documentation
The same key reduces correctly at every prime dividing the pivot. No field structure on the composite pivot ring is used.
```
theorem pivotResidueKey_mul_at_divisor (M : ℕ) [NeZero M] (L : ℕ) (v : ℤ)
    {p : ℕ} (hp : p ∣ M) (hL : L.Coprime M) :
    ((pivotResidueKey M L v).val : ZMod p) * (L : ZMod p) = (v : ZMod p) := by
…
```
Mentions: OAI.Ostmann.pivotResidueKey
theorem OAI.Ostmann.positiveIntegerPivotKey_mul_at_divisor line 34