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

instance Prod.instMul {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] : Mul (M × N)

Equations

• Prod.instMul = { mul := fun (p q : M × N) => (p.1 * q.1, p.2 * q.2) }

instance Prod.instAdd {M : Type u_6} {N : Type u_7} [Add M] [Add N] : Add (M × N)

Equations

• Prod.instAdd = { add := fun (p q : M × N) => (p.1 + q.1, p.2 + q.2) }

@[simp]

theorem Prod.fst_mul {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (p q : M × N) : (p * q).1 = p.1 * q.1

@[simp]

theorem Prod.fst_add {M : Type u_6} {N : Type u_7} [Add M] [Add N] (p q : M × N) : (p + q).1 = p.1 + q.1

@[simp]

theorem Prod.snd_mul {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (p q : M × N) : (p * q).2 = p.2 * q.2

@[simp]

theorem Prod.snd_add {M : Type u_6} {N : Type u_7} [Add M] [Add N] (p q : M × N) : (p + q).2 = p.2 + q.2

@[simp]

theorem Prod.mk_mul_mk {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (a₁ a₂ : M) (b₁ b₂ : N) : (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)

@[simp]

theorem Prod.mk_add_mk {M : Type u_6} {N : Type u_7} [Add M] [Add N] (a₁ a₂ : M) (b₁ b₂ : N) : (a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)

@[simp]

theorem Prod.swap_mul {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (p q : M × N) : (p * q).swap = p.swap * q.swap

@[simp]

theorem Prod.swap_add {M : Type u_6} {N : Type u_7} [Add M] [Add N] (p q : M × N) : (p + q).swap = p.swap + q.swap

theorem Prod.mul_def {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (p q : M × N) : p * q = (p.1 * q.1, p.2 * q.2)

theorem Prod.add_def {M : Type u_6} {N : Type u_7} [Add M] [Add N] (p q : M × N) : p + q = (p.1 + q.1, p.2 + q.2)

instance Prod.instInv {G : Type u_6} {H : Type u_7} [Inv G] [Inv H] : Inv (G × H)

Equations

• Prod.instInv = { inv := fun (p : G × H) => (p.1⁻¹, p.2⁻¹) }

instance Prod.instNeg {G : Type u_6} {H : Type u_7} [Neg G] [Neg H] : Neg (G × H)

Equations

• Prod.instNeg = { neg := fun (p : G × H) => (-p.1, -p.2) }

@[simp]

theorem Prod.fst_inv {G : Type u_6} {H : Type u_7} [Inv G] [Inv H] (p : G × H) : p⁻¹.1 = p.1⁻¹

@[simp]

theorem Prod.fst_neg {G : Type u_6} {H : Type u_7} [Neg G] [Neg H] (p : G × H) : (-p).1 = -p.1

@[simp]

theorem Prod.snd_inv {G : Type u_6} {H : Type u_7} [Inv G] [Inv H] (p : G × H) : p⁻¹.2 = p.2⁻¹

@[simp]

theorem Prod.snd_neg {G : Type u_6} {H : Type u_7} [Neg G] [Neg H] (p : G × H) : (-p).2 = -p.2

@[simp]

theorem Prod.inv_mk {G : Type u_6} {H : Type u_7} [Inv G] [Inv H] (a : G) (b : H) : (a, b)⁻¹ = (a⁻¹, b⁻¹)

@[simp]

theorem Prod.neg_mk {G : Type u_6} {H : Type u_7} [Neg G] [Neg H] (a : G) (b : H) : -(a, b) = (-a, -b)

@[simp]

theorem Prod.swap_inv {G : Type u_6} {H : Type u_7} [Inv G] [Inv H] (p : G × H) : p⁻¹.swap = p.swap⁻¹

@[simp]

theorem Prod.swap_neg {G : Type u_6} {H : Type u_7} [Neg G] [Neg H] (p : G × H) : (-p).swap = -p.swap

instance Prod.instDiv {G : Type u_6} {H : Type u_7} [Div G] [Div H] : Div (G × H)

Equations

• Prod.instDiv = { div := fun (p q : G × H) => (p.1 / q.1, p.2 / q.2) }

instance Prod.instSub {G : Type u_6} {H : Type u_7} [Sub G] [Sub H] : Sub (G × H)

Equations

• Prod.instSub = { sub := fun (p q : G × H) => (p.1 - q.1, p.2 - q.2) }

@[simp]

theorem Prod.fst_div {G : Type u_6} {H : Type u_7} [Div G] [Div H] (a b : G × H) : (a / b).1 = a.1 / b.1

@[simp]

theorem Prod.fst_sub {G : Type u_6} {H : Type u_7} [Sub G] [Sub H] (a b : G × H) : (a - b).1 = a.1 - b.1

@[simp]

theorem Prod.snd_div {G : Type u_6} {H : Type u_7} [Div G] [Div H] (a b : G × H) : (a / b).2 = a.2 / b.2

@[simp]

theorem Prod.snd_sub {G : Type u_6} {H : Type u_7} [Sub G] [Sub H] (a b : G × H) : (a - b).2 = a.2 - b.2

@[simp]

theorem Prod.mk_div_mk {G : Type u_6} {H : Type u_7} [Div G] [Div H] (x₁ x₂ : G) (y₁ y₂ : H) : (x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)

@[simp]

theorem Prod.mk_sub_mk {G : Type u_6} {H : Type u_7} [Sub G] [Sub H] (x₁ x₂ : G) (y₁ y₂ : H) : (x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)

@[simp]

theorem Prod.swap_div {G : Type u_6} {H : Type u_7} [Div G] [Div H] (a b : G × H) : (a / b).swap = a.swap / b.swap

@[simp]

theorem Prod.swap_sub {G : Type u_6} {H : Type u_7} [Sub G] [Sub H] (a b : G × H) : (a - b).swap = a.swap - b.swap

theorem Prod.div_def {G : Type u_6} {H : Type u_7} [Div G] [Div H] (a b : G × H) : a / b = (a.1 / b.1, a.2 / b.2)

theorem Prod.sub_def {G : Type u_6} {H : Type u_7} [Sub G] [Sub H] (a b : G × H) : a - b = (a.1 - b.1, a.2 - b.2)

instance Prod.instSMul {M : Type u_6} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul M β] : SMul M (α × β)

Equations

• Prod.instSMul = { smul := fun (a : M) (p : α × β) => (a • p.1, a • p.2) }

instance Prod.instVAdd {M : Type u_6} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd M β] : VAdd M (α × β)

Equations

• Prod.instVAdd = { vadd := fun (a : M) (p : α × β) => (a +ᵥ p.1, a +ᵥ p.2) }

@[simp]

theorem Prod.smul_fst {M : Type u_6} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul M β] (a : M) (x : α × β) : (a • x).1 = a • x.1

@[simp]

theorem Prod.vadd_fst {M : Type u_6} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd M β] (a : M) (x : α × β) : (a +ᵥ x).1 = a +ᵥ x.1

@[simp]

theorem Prod.smul_snd {M : Type u_6} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul M β] (a : M) (x : α × β) : (a • x).2 = a • x.2

@[simp]

theorem Prod.vadd_snd {M : Type u_6} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd M β] (a : M) (x : α × β) : (a +ᵥ x).2 = a +ᵥ x.2

@[simp]

theorem Prod.smul_mk {M : Type u_6} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul M β] (a : M) (b : α) (c : β) : a • (b, c) = (a • b, a • c)

@[simp]

theorem Prod.vadd_mk {M : Type u_6} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd M β] (a : M) (b : α) (c : β) : a +ᵥ (b, c) = (a +ᵥ b, a +ᵥ c)

theorem Prod.smul_def {M : Type u_6} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul M β] (a : M) (x : α × β) : a • x = (a • x.1, a • x.2)

theorem Prod.vadd_def {M : Type u_6} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd M β] (a : M) (x : α × β) : a +ᵥ x = (a +ᵥ x.1, a +ᵥ x.2)

@[simp]

theorem Prod.smul_swap {M : Type u_6} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul M β] (a : M) (x : α × β) : (a • x).swap = a • x.swap

@[simp]

theorem Prod.vadd_swap {M : Type u_6} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd M β] (a : M) (x : α × β) : (a +ᵥ x).swap = a +ᵥ x.swap

instance Prod.instPow {E : Type u_6} {α : Type u_7} {β : Type u_8} [Pow α E] [Pow β E] : Pow (α × β) E

Equations

• Prod.instPow = { pow := fun (p : α × β) (c : E) => (p.1 ^ c, p.2 ^ c) }

@[simp]

theorem Prod.pow_fst {E : Type u_6} {α : Type u_7} {β : Type u_8} [Pow α E] [Pow β E] (p : α × β) (c : E) : (p ^ c).1 = p.1 ^ c

@[simp]

theorem Prod.pow_snd {E : Type u_6} {α : Type u_7} {β : Type u_8} [Pow α E] [Pow β E] (p : α × β) (c : E) : (p ^ c).2 = p.2 ^ c

@[simp]

theorem Prod.pow_mk {E : Type u_6} {α : Type u_7} {β : Type u_8} [Pow α E] [Pow β E] (c : E) (a : α) (b : β) : (a, b) ^ c = (a ^ c, b ^ c)

theorem Prod.pow_def {E : Type u_6} {α : Type u_7} {β : Type u_8} [Pow α E] [Pow β E] (p : α × β) (c : E) : p ^ c = (p.1 ^ c, p.2 ^ c)

@[simp]

theorem Prod.pow_swap {E : Type u_6} {α : Type u_7} {β : Type u_8} [Pow α E] [Pow β E] (p : α × β) (c : E) : (p ^ c).swap = p.swap ^ c