Residues modulo two and modulo powers of two

A residue modulo two is 0 or 1, so its canonical representative ZMod.val is the indicator of being nonzero. This is the identity behind the counting arguments that read a ℕ-valued weight off a ZMod 2-valued vector: summing the representatives of the coordinates counts the nonzero ones.

In ℤ/2^n the element 2 is nilpotent, so in ℤ/2^{k+1} the units are exactly the odd elements: an even element plus a unit is a unit, and an even element is never a unit.

Main results

• ZMod.val_eq_ite_mod_two: a.val = if a ≠ 0 then 1 else 0 for a : ZMod 2.
• ZMod.isNilpotent_two: 2 is nilpotent in ℤ/2^n.
• ZMod.isUnit_two_mul_add: 2c + u is a unit in ℤ/2^{k+1} when u is.
• ZMod.not_isUnit_two_mul: 2c is not a unit in ℤ/2^{k+1}.
• ZMod.eq_two_mul_or_eq_two_mul_add_one: every element of ℤ/2^{k+1} is even or odd.

theorem ZMod.val_eq_ite_mod_two (a : ZMod 2) : a.val = if a ≠ 0 then 1 else 0

The representative of a residue modulo two is the indicator of being nonzero.

theorem ZMod.isNilpotent_two {n : ℕ} : IsNilpotent 2

2 is nilpotent modulo a power of two: 2 ^ n = 0 in ℤ/2^n.

theorem ZMod.isUnit_two_mul_add {k : ℕ} {c u : ZMod (2 ^ (k + 1))} (hu : IsUnit u) : IsUnit (2 * c + u)

An even element plus a unit is a unit in ℤ/2^{k+1}.

theorem ZMod.not_isUnit_two_mul {k : ℕ} (c : ZMod (2 ^ (k + 1))) : ¬IsUnit (2 * c)

An even element of ℤ/2^{k+1} is not a unit.

theorem ZMod.eq_two_mul_or_eq_two_mul_add_one {k : ℕ} (x : ZMod (2 ^ (k + 1))) : (∃ (c : ZMod (2 ^ (k + 1))), x = 2 * c) ∨ ∃ (c : ZMod (2 ^ (k + 1))), x = 2 * c + 1

Every element of ℤ/2^{k+1} is even or odd, according to the parity of an integer lift.