Parity and Hamming weight

The parity of a bit string is the parity of its Hamming weight (Cslib.parity_eq_decide_weight), so parity is a symmetric Boolean function (Cslib.isSymmetric_parity). This bridge is kept apart from both BitString.Parity and BitString.Weight, so that neither of them imports the other.

Main results

• Cslib.parity_eq_decide_weight: parity is the parity of the weight.
• Cslib.isSymmetric_parity: parity is symmetric.

theorem Cslib.parity_eq_decide_weight {n : ℕ} (x : BitString n) : parity n x = decide (BitString.weight x % 2 = 1)

Parity is the parity of the weight.

theorem Cslib.isSymmetric_parity {n : ℕ} : (parity n).IsSymmetric

Parity is symmetric.