ProjectionPairFiber.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The two fibers of reduction modulo half the order

Reduction from ZMod (2 * m) to ZMod m has exactly the two usual lifts of each element when m is positive.

theorem OAI.CirculantHadamard.zmod_double_cast_eq_iff line 16

Source documentation

The fiber of reduction modulo m consists of its two canonical lifts.

theorem zmod_double_cast_eq_iff {m : ℕ} (hm : 0 < m) (h : m ∣ 2 * m)
    (x : ZMod (2 * m)) (j : ZMod m) :
    ZMod.castHom h (ZMod m) x = j ↔
      x = (j.val : ZMod (2 * m)) ∨ x = ((j.val + m : ℕ) : ZMod (2 * m)) := by
…

theorem OAI.CirculantHadamard.zmod_double_lifts_ne line 46
Source documentation
The two canonical lifts into the group of twice the order are distinct.
```
theorem zmod_double_lifts_ne {m : ℕ} (hm : 0 < m) (j : ZMod m) :
    (j.val : ZMod (2 * m)) ≠ ((j.val + m : ℕ) : ZMod (2 * m)) := by
…
```