The two-element field ZMod 2 as bits

Bits form the two-element field under exclusive or and conjunction (Mathlib's BooleanRing Bool). The computable ring isomorphism Cslib.BitString.bitEquiv : ZMod 2 ≃+* Bool identifies ZMod 2 with Bool; it equals Mathlib's ZMod.ringEquivOfPrime (Cslib.BitString.bitEquiv_eq_ringEquivOfPrime), and its inverse reads a bit as 0 or 1 in ZMod 2, matching Cslib.BitString.bitVal (ZMod 2) (Cslib.BitString.bitEquiv_symm_apply).

Main definitions

• Cslib.BitString.bitEquiv: the computable ring isomorphism ZMod 2 ≃+* Bool.

Main results

• Cslib.BitString.bitEquiv_eq_ringEquivOfPrime: bitEquiv is ZMod.ringEquivOfPrime Bool.
• Cslib.BitString.bitEquiv_symm_apply, Cslib.BitString.bitEquiv_symm_false, Cslib.BitString.bitEquiv_symm_true: bitEquiv.symm reads false as 0 and true as 1.

References

• R. Lidl, H. Niederreiter, Finite Fields, Chapter 1

def Cslib.BitString.bitEquiv : ZMod 2 ≃+* Bool

The two-element field 𝔽₂ = ZMod 2 as bits: the unique ring isomorphism ZMod 2 ≃+* Bool.

theorem Cslib.BitString.bitEquiv_eq_ringEquivOfPrime : bitEquiv = ZMod.ringEquivOfPrime Bool Nat.prime_two bitEquiv_eq_ringEquivOfPrime._proof_1

bitEquiv is Mathlib's ZMod.ringEquivOfPrime for the two-element field Bool, as a computable definition.

theorem Cslib.BitString.bitEquiv_symm_apply (b : Bool) : bitEquiv.symm b = bitVal (ZMod 2) b

bitEquiv.symm reads a bit as 0 or 1, as Cslib.BitString.bitVal does.

@[simp]

theorem Cslib.BitString.bitEquiv_symm_false : bitEquiv.symm false = 0

bitEquiv.symm reads the bit false as 0.

@[simp]

theorem Cslib.BitString.bitEquiv_symm_true : bitEquiv.symm true = 1

bitEquiv.symm reads the bit true as 1.