Stream: Beginner Questions

Topic: Proving things about a definition of a record

Robert Shlyakhtenko (May 28 2025 at 01:09):

I have defined $\mathbb{Z}/2\mathbb{Z}$ as follows:

  "Z2 = ⦇
     carrier = {0,1},
     mult = (λx y. (x + y) mod 2),
     one = 0
   ⦈"

I would like to prove certain things about Z2; for example, that it is a group. The following is giving me trouble: how do I prove that for any fixed $x, y \in$ carrier Z2,

(mult Z2 x y) = ((x + y) mod 2)

And in general, is there an easy way to convert a proof about addition mod 2 into a proof about the "mult Z2" that I have defined?

Many thanks.

Last updated: May 31 2025 at 04:25 UTC