Arithmetic operators on (pairwise) product types #
This file provides only the notation for (componentwise) 0, 1, +, *, •, ^, ⁻¹ on
(pairwise) product types. See Mathlib/Algebra/Group/Prod.lean for the Monoid and Group
instances. There is also an instance of the Star notation typeclass, but no default notation is
included.
@[implicit_reducible]
@[implicit_reducible]
@[simp]
@[simp]
@[simp]
@[simp]
@[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]
@[simp]
@[implicit_reducible]
@[implicit_reducible]
@[simp]
theorem
Prod.fst_mul
{M : Type u_8}
{N : Type u_9}
[Mul M]
[Mul N]
(p q : M × N)
:
(p * q).1 = p.1 * q.1
@[simp]
theorem
Prod.fst_add
{M : Type u_8}
{N : Type u_9}
[Add M]
[Add N]
(p q : M × N)
:
(p + q).1 = p.1 + q.1
@[simp]
theorem
Prod.snd_mul
{M : Type u_8}
{N : Type u_9}
[Mul M]
[Mul N]
(p q : M × N)
:
(p * q).2 = p.2 * q.2
@[simp]
theorem
Prod.snd_add
{M : Type u_8}
{N : Type u_9}
[Add M]
[Add N]
(p q : M × N)
:
(p + q).2 = p.2 + q.2
@[simp]
theorem
Prod.mk_mul_mk
{M : Type u_8}
{N : Type u_9}
[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_8}
{N : Type u_9}
[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_8}
{N : Type u_9}
[Mul M]
[Mul N]
(p q : M × N)
:
(p * q).swap = p.swap * q.swap
@[simp]
theorem
Prod.swap_add
{M : Type u_8}
{N : Type u_9}
[Add M]
[Add N]
(p q : M × N)
:
(p + q).swap = p.swap + q.swap
theorem
Prod.mul_def
{M : Type u_8}
{N : Type u_9}
[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_8}
{N : Type u_9}
[Add M]
[Add N]
(p q : M × N)
:
p + q = (p.1 + q.1, p.2 + q.2)
@[implicit_reducible]
@[implicit_reducible]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[implicit_reducible]
@[implicit_reducible]
@[simp]
theorem
Prod.fst_div
{G : Type u_8}
{H : Type u_9}
[Div G]
[Div H]
(a b : G × H)
:
(a / b).1 = a.1 / b.1
@[simp]
theorem
Prod.fst_sub
{G : Type u_8}
{H : Type u_9}
[Sub G]
[Sub H]
(a b : G × H)
:
(a - b).1 = a.1 - b.1
@[simp]
theorem
Prod.snd_div
{G : Type u_8}
{H : Type u_9}
[Div G]
[Div H]
(a b : G × H)
:
(a / b).2 = a.2 / b.2
@[simp]
theorem
Prod.snd_sub
{G : Type u_8}
{H : Type u_9}
[Sub G]
[Sub H]
(a b : G × H)
:
(a - b).2 = a.2 - b.2
@[simp]
theorem
Prod.mk_div_mk
{G : Type u_8}
{H : Type u_9}
[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_8}
{H : Type u_9}
[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_8}
{H : Type u_9}
[Div G]
[Div H]
(a b : G × H)
:
(a / b).swap = a.swap / b.swap
@[simp]
theorem
Prod.swap_sub
{G : Type u_8}
{H : Type u_9}
[Sub G]
[Sub H]
(a b : G × H)
:
(a - b).swap = a.swap - b.swap
theorem
Prod.div_def
{G : Type u_8}
{H : Type u_9}
[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_8}
{H : Type u_9}
[Sub G]
[Sub H]
(a b : G × H)
:
a - b = (a.1 - b.1, a.2 - b.2)
@[implicit_reducible]
instance
Prod.instPow
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[Pow α E]
[Pow β E]
:
Pow (α × β) E
@[implicit_reducible]
@[implicit_reducible]
instance
Prod.instSMul
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[SMul E α]
[SMul E β]
:
SMul E (α × β)
@[simp]
theorem
Prod.pow_fst
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[Pow α E]
[Pow β E]
(p : α × β)
(c : E)
:
(p ^ c).1 = p.1 ^ c
@[simp]
@[simp]
theorem
Prod.smul_fst
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[SMul E α]
[SMul E β]
(c : E)
(p : α × β)
:
(c • p).1 = c • p.1
@[simp]
theorem
Prod.pow_snd
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[Pow α E]
[Pow β E]
(p : α × β)
(c : E)
:
(p ^ c).2 = p.2 ^ c
@[simp]
theorem
Prod.smul_snd
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[SMul E α]
[SMul E β]
(c : E)
(p : α × β)
:
(c • p).2 = c • p.2
@[simp]
@[simp]
theorem
Prod.pow_mk
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[Pow α E]
[Pow β E]
(a : α)
(b : β)
(c : E)
:
(a, b) ^ c = (a ^ c, b ^ c)
@[simp]
theorem
Prod.smul_mk
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[SMul E α]
[SMul E β]
(c : E)
(a : α)
(b : β)
:
c • (a, b) = (c • a, c • b)
theorem
Prod.pow_def
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[Pow α E]
[Pow β E]
(p : α × β)
(c : E)
:
p ^ c = (p.1 ^ c, p.2 ^ c)
theorem
Prod.smul_def
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[SMul E α]
[SMul E β]
(c : E)
(p : α × β)
:
c • p = (c • p.1, c • p.2)
@[simp]
theorem
Prod.pow_swap
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[Pow α E]
[Pow β E]
(p : α × β)
(c : E)
:
(p ^ c).swap = p.swap ^ c
@[simp]
theorem
Prod.smul_swap
{E : Type u_8}
{α : Type u_9}
{β : Type u_10}
[SMul E α]
[SMul E β]
(c : E)
(p : α × β)
:
(c • p).swap = c • p.swap
@[simp]
@[implicit_reducible]
@[simp]
@[simp]