Zero and One instances on M × N

In this file we define 0 and 1 on M × N as the pair (0, 0) and (1, 1) respectively. We also prove trivial simp lemmas:

instance Prod.instOne {M : Type u_3} {N : Type u_4} [One M] [One N] : One (M × N)

Equations

• Prod.instOne = { one := (1, 1) }

instance Prod.instZero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] : Zero (M × N)

Equations

• Prod.instZero = { zero := (0, 0) }

@[simp]

theorem Prod.fst_one {M : Type u_3} {N : Type u_4} [One M] [One N] : 1.1 = 1

@[simp]

theorem Prod.fst_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] : 0.1 = 0

@[simp]

theorem Prod.snd_one {M : Type u_3} {N : Type u_4} [One M] [One N] : 1.2 = 1

@[simp]

theorem Prod.snd_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] : 0.2 = 0

theorem Prod.one_eq_mk {M : Type u_3} {N : Type u_4} [One M] [One N] : 1 = (1, 1)

theorem Prod.zero_eq_mk {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] : 0 = (0, 0)

@[simp]

theorem Prod.mk_one_one {M : Type u_3} {N : Type u_4} [One M] [One N] : (1, 1) = 1

@[simp]

theorem Prod.mk_zero_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] : (0, 0) = 0

@[simp]

theorem Prod.mk_eq_one {M : Type u_3} {N : Type u_4} [One M] [One N] {x : M} {y : N} : (x, y) = 1 ↔ x = 1 ∧ y = 1

@[simp]

theorem Prod.mk_eq_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {x : M} {y : N} : (x, y) = 0 ↔ x = 0 ∧ y = 0

@[simp]

theorem Prod.swap_one {M : Type u_3} {N : Type u_4} [One M] [One N] : swap 1 = 1

@[simp]

theorem Prod.swap_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] : swap 0 = 0