Documentation

Mathlib.Algebra.Notation.Prod

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:

source
instance Prod.instOne {M : Type u_3} {N : Type u_4} [One M] [One N] :
One (M × N)
Equations
    source
    instance Prod.instZero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
    Zero (M × N)
    Equations
      source
      @[simp]
      theorem Prod.fst_one {M : Type u_3} {N : Type u_4} [One M] [One N] :
      1.1 = 1
      source
      @[simp]
      theorem Prod.fst_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
      0.1 = 0
      source
      @[simp]
      theorem Prod.snd_one {M : Type u_3} {N : Type u_4} [One M] [One N] :
      1.2 = 1
      source
      @[simp]
      theorem Prod.snd_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
      0.2 = 0
      source
      theorem Prod.one_eq_mk {M : Type u_3} {N : Type u_4} [One M] [One N] :
      1 = (1, 1)
      source
      theorem Prod.zero_eq_mk {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
      0 = (0, 0)
      source
      theorem Prod.mk_one_one {M : Type u_3} {N : Type u_4} [One M] [One N] :
      (1, 1) = 1
      source
      theorem Prod.mk_zero_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
      (0, 0) = 0
      source
      @[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
      source
      @[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
      source
      @[simp]
      theorem Prod.swap_one {M : Type u_3} {N : Type u_4} [One M] [One N] :
      swap 1 = 1
      source
      @[simp]
      theorem Prod.swap_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
      swap 0 = 0
      source
      instance Prod.instMul {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] :
      Mul (M × N)
      Equations
        source
        instance Prod.instAdd {M : Type u_6} {N : Type u_7} [Add M] [Add N] :
        Add (M × N)
        Equations
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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₂)
          source
          @[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₂)
          source
          @[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
          source
          @[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
          source
          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)
          source
          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)
          source
          instance Prod.instInv {G : Type u_6} {H : Type u_7} [Inv G] [Inv H] :
          Inv (G × H)
          Equations
            source
            instance Prod.instNeg {G : Type u_6} {H : Type u_7} [Neg G] [Neg H] :
            Neg (G × H)
            Equations
              source
              @[simp]
              theorem Prod.fst_inv {G : Type u_6} {H : Type u_7} [Inv G] [Inv H] (p : G × H) :
              p⁻¹.1 = p.1⁻¹
              source
              @[simp]
              theorem Prod.fst_neg {G : Type u_6} {H : Type u_7} [Neg G] [Neg H] (p : G × H) :
              (-p).1 = -p.1
              source
              @[simp]
              theorem Prod.snd_inv {G : Type u_6} {H : Type u_7} [Inv G] [Inv H] (p : G × H) :
              p⁻¹.2 = p.2⁻¹
              source
              @[simp]
              theorem Prod.snd_neg {G : Type u_6} {H : Type u_7} [Neg G] [Neg H] (p : G × H) :
              (-p).2 = -p.2
              source
              @[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⁻¹)
              source
              @[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)
              source
              @[simp]
              theorem Prod.swap_inv {G : Type u_6} {H : Type u_7} [Inv G] [Inv H] (p : G × H) :
              p⁻¹.swap = p.swap⁻¹
              source
              @[simp]
              theorem Prod.swap_neg {G : Type u_6} {H : Type u_7} [Neg G] [Neg H] (p : G × H) :
              (-p).swap = -p.swap
              source
              instance Prod.instDiv {G : Type u_6} {H : Type u_7} [Div G] [Div H] :
              Div (G × H)
              Equations
                source
                instance Prod.instSub {G : Type u_6} {H : Type u_7} [Sub G] [Sub H] :
                Sub (G × H)
                Equations
                  source
                  @[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
                  source
                  @[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
                  source
                  @[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
                  source
                  @[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
                  source
                  @[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₂)
                  source
                  @[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₂)
                  source
                  @[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
                  source
                  @[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
                  source
                  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)
                  source
                  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)
                  source
                  instance Prod.instSMul {M : Type u_6} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul M β] :
                  SMul M (α × β)
                  Equations
                    source
                    instance Prod.instVAdd {M : Type u_6} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd M β] :
                    VAdd M (α × β)
                    Equations
                      source
                      @[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
                      source
                      @[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
                      source
                      @[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
                      source
                      @[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
                      source
                      @[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)
                      source
                      @[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)
                      source
                      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)
                      source
                      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)
                      source
                      @[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
                      source
                      @[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
                      source
                      instance Prod.instPow {E : Type u_6} {α : Type u_7} {β : Type u_8} [Pow α E] [Pow β E] :
                      Pow (α × β) E
                      Equations
                        source
                        @[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
                        source
                        @[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
                        source
                        @[simp]
                        theorem Prod.pow_mk {E : Type u_6} {α : Type u_7} {β : Type u_8} [Pow α E] [Pow β E] (a : α) (b : β) (c : E) :
                        (a, b) ^ c = (a ^ c, b ^ c)
                        source
                        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)
                        source
                        @[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