Mathlib.Algebra.Notation.Prod

Prod.instOne instance

: One (M × N)

Full source

@[to_additive]
instance instOne : One (M × N) :=
  ⟨(1, 1)⟩

Multiplicative Identity on Product Types

Informal description

For any types $M$ and $N$ each equipped with a multiplicative identity element $1$, the product type $M \times N$ has a multiplicative identity given by $(1, 1)$.

Prod.fst_one theorem

: (1 : M × N).1 = 1

Full source

@[to_additive (attr := simp)]
theorem fst_one : (1 : M × N).1 = 1 :=
  rfl

First Projection of Product Identity Equals Identity

Informal description

For any types $M$ and $N$ with multiplicative identities, the first projection of the multiplicative identity $(1,1)$ in $M \times N$ equals the multiplicative identity in $M$, i.e., $(1 : M \times N).1 = 1$.

Prod.snd_one theorem

: (1 : M × N).2 = 1

Full source

@[to_additive (attr := simp)]
theorem snd_one : (1 : M × N).2 = 1 :=
  rfl

Second Projection of Product Identity Equals Identity

Informal description

For any types $M$ and $N$ with multiplicative identities, the second projection of the multiplicative identity $(1,1)$ in $M \times N$ equals the multiplicative identity in $N$, i.e., $(1 : M \times N).2 = 1$.

Prod.one_eq_mk theorem

: (1 : M × N) = (1, 1)

Full source

@[to_additive]
theorem one_eq_mk : (1 : M × N) = (1, 1) :=
  rfl

Product Identity as Pair of Identities

Informal description

For any types $M$ and $N$ each equipped with a multiplicative identity element $1$, the multiplicative identity in the product type $M \times N$ is equal to the pair $(1, 1)$, i.e., $1 = (1, 1)$.

Prod.mk_one_one theorem

: ((1 : M), (1 : N)) = 1

Full source

@[to_additive (attr := simp)]
theorem mk_one_one : ((1 : M), (1 : N)) = 1 := rfl

Pair of Identities Equals Product Identity in $M \times N$

Informal description

For any types $M$ and $N$ each equipped with a multiplicative identity element $1$, the pair $(1_M, 1_N)$ is equal to the multiplicative identity $1$ in the product type $M \times N$.

Prod.mk_eq_one theorem

{x : M} {y : N} : (x, y) = 1 ↔ x = 1 ∧ y = 1

Full source

@[to_additive (attr := simp)]
theorem mk_eq_one {x : M} {y : N} : (x, y)(x, y) = 1 ↔ x = 1 ∧ y = 1 := mk_inj

Pair Equals Identity if and only if Components Equal Identity: $(x, y) = 1 ↔ x = 1 ∧ y = 1$

Informal description

For any elements $x$ in $M$ and $y$ in $N$, the pair $(x, y)$ equals the multiplicative identity $1$ in $M \times N$ if and only if $x = 1$ in $M$ and $y = 1$ in $N$.

Prod.swap_one theorem

: (1 : M × N).swap = 1

Full source

@[to_additive (attr := simp)]
theorem swap_one : (1 : M × N).swap = 1 :=
  rfl

Swap Preserves Multiplicative Identity in Product Types

Informal description

For any types $M$ and $N$ each equipped with a multiplicative identity element $1$, swapping the components of the multiplicative identity $(1, 1)$ in $M \times N$ yields the multiplicative identity again, i.e., $(1, 1).\text{swap} = (1, 1) = 1$.

Prod.instMul instance

: Mul (M × N)

Full source

@[to_additive]
instance instMul : Mul (M × N) :=
  ⟨fun p q => ⟨p.1 * q.1, p.2 * q.2⟩⟩

Componentwise Multiplication on Product Types

Informal description

For any types $M$ and $N$ with multiplication operations, the product type $M \times N$ can be equipped with a multiplication operation defined componentwise: $(x_1, y_1) \cdot (x_2, y_2) = (x_1 \cdot x_2, y_1 \cdot y_2)$.

Prod.fst_mul theorem

(p q : M × N) : (p * q).1 = p.1 * q.1

Full source

@[to_additive (attr := simp)]
theorem fst_mul (p q : M × N) : (p * q).1 = p.1 * q.1 := rfl

First Component of Product in $M \times N$

Informal description

For any elements $p$ and $q$ in the product type $M \times N$, the first component of their product is equal to the product of their first components, i.e., $(p \cdot q)_1 = p_1 \cdot q_1$.

Prod.snd_mul theorem

(p q : M × N) : (p * q).2 = p.2 * q.2

Full source

@[to_additive (attr := simp)]
theorem snd_mul (p q : M × N) : (p * q).2 = p.2 * q.2 := rfl

Second Component Preserves Multiplication in Product Types

Informal description

For any elements $p$ and $q$ in the product type $M \times N$, the second component of their product is equal to the product of their second components, i.e., $(p \cdot q)_2 = p_2 \cdot q_2$.

Prod.mk_mul_mk theorem

(a₁ a₂ : M) (b₁ b₂ : N) : (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)

Full source

@[to_additive (attr := simp)]
theorem mk_mul_mk (a₁ a₂ : M) (b₁ b₂ : N) : (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂) := rfl

Componentwise Multiplication of Pairs: $(a₁, b₁) \cdot (a₂, b₂) = (a₁ \cdot a₂, b₁ \cdot b₂)$

Informal description

For any elements $a₁, a₂$ in $M$ and $b₁, b₂$ in $N$, the product of the pairs $(a₁, b₁)$ and $(a₂, b₂)$ in $M \times N$ is given by $(a₁ \cdot a₂, b₁ \cdot b₂)$.

Prod.swap_mul theorem

(p q : M × N) : (p * q).swap = p.swap * q.swap

Full source

@[to_additive (attr := simp)]
theorem swap_mul (p q : M × N) : (p * q).swap = p.swap * q.swap := rfl

Swap of Product Equals Product of Swaps in $M \times N$

Informal description

For any elements $p$ and $q$ in the product type $M \times N$, the swap of their product equals the product of their swaps, i.e., $(p \cdot q).\text{swap} = p.\text{swap} \cdot q.\text{swap}$.

Prod.mul_def theorem

(p q : M × N) : p * q = (p.1 * q.1, p.2 * q.2)

Full source

@[to_additive]
theorem mul_def (p q : M × N) : p * q = (p.1 * q.1, p.2 * q.2) := rfl

Componentwise Multiplication in Product Types

Informal description

For any elements $p = (x_1, y_1)$ and $q = (x_2, y_2)$ in the product type $M \times N$, their product is given by componentwise multiplication: $p \cdot q = (x_1 \cdot x_2, y_1 \cdot y_2)$.

Prod.instInv instance

: Inv (G × H)

Full source

@[to_additive]
instance instInv : Inv (G × H) :=
  ⟨fun p => (p.1⁻¹, p.2⁻¹)⟩

Componentwise Inversion on Product Types

Informal description

For any types $G$ and $H$ equipped with inversion operations, the product type $G \times H$ is also equipped with an inversion operation defined componentwise: $(x, y)^{-1} = (x^{-1}, y^{-1})$.

Prod.fst_inv theorem

(p : G × H) : p⁻¹.1 = p.1⁻¹

Full source

@[to_additive (attr := simp)]
theorem fst_inv (p : G × H) : p⁻¹.1 = p.1⁻¹ := rfl

First Component of Inverse in Product Type

Informal description

For any pair $p = (x, y)$ in the product type $G \times H$ where $G$ and $H$ are types equipped with inversion operations, the first component of the inverse of $p$ is equal to the inverse of the first component of $p$, i.e., $(p^{-1})_1 = x^{-1}$.

Prod.snd_inv theorem

(p : G × H) : p⁻¹.2 = p.2⁻¹

Full source

@[to_additive (attr := simp)]
theorem snd_inv (p : G × H) : p⁻¹.2 = p.2⁻¹ := rfl

Second Component of Inverse in Product Type

Informal description

For any pair $p = (x, y)$ in the product type $G \times H$ where $G$ and $H$ are types equipped with inversion operations, the second component of the inverse of $p$ is equal to the inverse of the second component of $p$, i.e., $(p^{-1})_2 = y^{-1}$.

Prod.inv_mk theorem

(a : G) (b : H) : (a, b)⁻¹ = (a⁻¹, b⁻¹)

Full source

@[to_additive (attr := simp)]
theorem inv_mk (a : G) (b : H) : (a, b)(a, b)⁻¹ = (a⁻¹, b⁻¹) := rfl

Inverse of Pair is Pair of Inverses

Informal description

For any elements $a$ in $G$ and $b$ in $H$, where $G$ and $H$ are types equipped with inversion operations, the inverse of the pair $(a, b)$ in the product type $G \times H$ is equal to the pair of inverses $(a^{-1}, b^{-1})$.

Prod.swap_inv theorem

(p : G × H) : p⁻¹.swap = p.swap⁻¹

Full source

@[to_additive (attr := simp)]
theorem swap_inv (p : G × H) : p⁻¹.swap = p.swap⁻¹ := rfl

Inverse Commutes with Swap in Product Type

Informal description

For any pair $p = (x, y)$ in the product type $G \times H$ where $G$ and $H$ are types equipped with inversion operations, swapping the components of the inverse of $p$ is equal to the inverse of the swapped components of $p$, i.e., $(p^{-1})_{\text{swap}} = (p_{\text{swap}})^{-1}$.

Prod.instDiv instance

: Div (G × H)

Full source

@[to_additive]
instance instDiv : Div (G × H) :=
  ⟨fun p q => ⟨p.1 / q.1, p.2 / q.2⟩⟩

Componentwise Division on Product Types

Informal description

For any two types $G$ and $H$ each equipped with a division operation, the product type $G \times H$ is also equipped with a division operation defined componentwise: $(a_1, a_2) / (b_1, b_2) = (a_1 / b_1, a_2 / b_2)$.

Prod.fst_div theorem

(a b : G × H) : (a / b).1 = a.1 / b.1

Full source

@[to_additive (attr := simp)]
theorem fst_div (a b : G × H) : (a / b).1 = a.1 / b.1 := rfl

First Component of Division in Product Type

Informal description

For any elements $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in the product type $G \times H$, the first component of their division is equal to the division of their first components, i.e., $(a / b).1 = a_1 / b_1$.

Prod.snd_div theorem

(a b : G × H) : (a / b).2 = a.2 / b.2

Full source

@[to_additive (attr := simp)]
theorem snd_div (a b : G × H) : (a / b).2 = a.2 / b.2 := rfl

Second Component of Division in Product Type

Informal description

For any elements $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in the product type $G \times H$, the second component of their division is equal to the division of their second components, i.e., $(a / b).2 = a_2 / b_2$.

Prod.mk_div_mk theorem

(x₁ x₂ : G) (y₁ y₂ : H) : (x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)

Full source

@[to_additive (attr := simp)]
theorem mk_div_mk (x₁ x₂ : G) (y₁ y₂ : H) : (x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂) := rfl

Componentwise Division Formula for Product Types

Informal description

For any elements $x₁, x₂$ in $G$ and $y₁, y₂$ in $H$, the division of the pairs $(x₁, y₁)$ and $(x₂, y₂)$ in the product type $G \times H$ is given by $(x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)$.

Prod.swap_div theorem

(a b : G × H) : (a / b).swap = a.swap / b.swap

Full source

@[to_additive (attr := simp)]
theorem swap_div (a b : G × H) : (a / b).swap = a.swap / b.swap := rfl

Swap Commutes with Componentwise Division in Product Types

Informal description

For any elements $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in the product type $G \times H$, swapping the components of their division is equal to the division of their swapped components, i.e., $(a / b).\text{swap} = a.\text{swap} / b.\text{swap}$ where $\text{swap}(x,y) = (y,x)$.

Prod.div_def theorem

(a b : G × H) : a / b = (a.1 / b.1, a.2 / b.2)

Full source

@[to_additive] lemma div_def (a b : G × H) : a / b = (a.1 / b.1, a.2 / b.2) := rfl

Componentwise Division Definition for Product Types

Informal description

For any elements $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in the product type $G \times H$, the division operation is defined componentwise as $a / b = (a_1 / b_1, a_2 / b_2)$.

Prod.instSMul instance

: SMul M (α × β)

Full source

@[to_additive]
instance instSMul : SMul M (α × β) where smul a p := (a • p.1, a • p.2)

Componentwise Scalar Multiplication on Product Types

Informal description

For any types $M$, $\alpha$, and $\beta$ where $M$ has a scalar multiplication operation with $\alpha$ and $\beta$, the product type $\alpha \times \beta$ inherits a scalar multiplication structure defined componentwise as $a \bullet (x, y) = (a \bullet x, a \bullet y)$.

Prod.smul_fst theorem

(a : M) (x : α × β) : (a • x).1 = a • x.1

Full source

@[to_additive (attr := simp)] lemma smul_fst (a : M) (x : α × β) : (a • x).1 = a • x.1 := rfl

First Component of Scalar Multiplication on Product Types

Informal description

For any scalar $a \in M$ and any pair $x = (x_1, x_2) \in \alpha \times \beta$, the first component of the scalar product $a \bullet x$ is equal to the scalar product of $a$ with the first component of $x$, i.e., $(a \bullet x)_1 = a \bullet x_1$.

Prod.smul_snd theorem

(a : M) (x : α × β) : (a • x).2 = a • x.2

Full source

@[to_additive (attr := simp)] lemma smul_snd (a : M) (x : α × β) : (a • x).2 = a • x.2 := rfl

Second Component of Scalar Multiplication on Product Types

Informal description

For any scalar $a \in M$ and any pair $x = (x_1, x_2) \in \alpha \times \beta$, the second component of the scalar product $a \bullet x$ is equal to the scalar product of $a$ with the second component of $x$, i.e., $(a \bullet x)_2 = a \bullet x_2$.

Prod.smul_mk theorem

(a : M) (b : α) (c : β) : a • (b, c) = (a • b, a • c)

Full source

@[to_additive (attr := simp)]
lemma smul_mk (a : M) (b : α) (c : β) : a • (b, c) = (a • b, a • c) := rfl

Componentwise Scalar Multiplication on Pairs: $a \bullet (b, c) = (a \bullet b, a \bullet c)$

Informal description

For any scalar $a \in M$ and elements $b \in \alpha$, $c \in \beta$, the scalar multiplication of $a$ with the pair $(b, c)$ is equal to the pair $(a \bullet b, a \bullet c)$, where $\bullet$ denotes the scalar multiplication operation in the respective types.

Prod.smul_def theorem

(a : M) (x : α × β) : a • x = (a • x.1, a • x.2)

Full source

@[to_additive]
lemma smul_def (a : M) (x : α × β) : a • x = (a • x.1, a • x.2) := rfl

Componentwise Scalar Multiplication on Pairs: $a \bullet (x_1, x_2) = (a \bullet x_1, a \bullet x_2)$

Informal description

For any scalar $a \in M$ and any pair $(x_1, x_2) \in \alpha \times \beta$, the scalar multiplication $a \bullet (x_1, x_2)$ is equal to $(a \bullet x_1, a \bullet x_2)$, where $\bullet$ denotes the scalar multiplication operation in the respective types.

Prod.smul_swap theorem

(a : M) (x : α × β) : (a • x).swap = a • x.swap

Full source

@[to_additive (attr := simp)] lemma smul_swap (a : M) (x : α × β) : (a • x).swap = a • x.swap := rfl

Scalar Multiplication Commutes with Pair Swapping: $(a \bullet x).\text{swap} = a \bullet x.\text{swap}$

Informal description

For any scalar $a \in M$ and any pair $x = (x_1, x_2) \in \alpha \times \beta$, the swap of the scalar multiplication $a \bullet x$ is equal to the scalar multiplication of $a$ with the swapped pair, i.e., $(a \bullet x).\text{swap} = a \bullet x.\text{swap}$.

Prod.instPow instance

: Pow (α × β) E

Full source

@[to_additive existing instSMul]
instance instPow : Pow (α × β) E where pow p c := (p.1 ^ c, p.2 ^ c)

Power Operation on Product Types

Informal description

For any types $\alpha$ and $\beta$ with a power operation defined by type $E$, the product type $\alpha \times \beta$ inherits a power operation where $(x, y)^n = (x^n, y^n)$ for any $(x, y) \in \alpha \times \beta$ and $n \in E$.

Prod.pow_fst theorem

(p : α × β) (c : E) : (p ^ c).fst = p.fst ^ c

Full source

@[to_additive existing (attr := simp) (reorder := 6 7) smul_fst]
lemma pow_fst (p : α × β) (c : E) : (p ^ c).fst = p.fst ^ c := rfl

First Component of Product Power: $(p^c).1 = x^c$

Informal description

For any pair $p = (x, y) \in \alpha \times \beta$ and any exponent $c \in E$, the first component of $p^c$ is equal to $x^c$, i.e., $(p^c).1 = x^c$.

Prod.pow_snd theorem

(p : α × β) (c : E) : (p ^ c).snd = p.snd ^ c

Full source

@[to_additive existing (attr := simp) (reorder := 6 7) smul_snd]
lemma pow_snd (p : α × β) (c : E) : (p ^ c).snd = p.snd ^ c := rfl

Second Component of Power in Product Type: $(p^c).2 = b^c$

Informal description

For any pair $p = (a, b)$ in the product type $\alpha \times \beta$ and any exponent $c \in E$, the second component of the power $p^c$ is equal to the power of the second component of $p$, i.e., $(p^c).2 = b^c$.

Prod.pow_mk theorem

(a : α) (b : β) (c : E) : Prod.mk a b ^ c = Prod.mk (a ^ c) (b ^ c)

Full source

@[to_additive existing (attr := simp) (reorder := 6 7 8) smul_mk]
lemma pow_mk (a : α) (b : β) (c : E) : Prod.mk a b ^ c = Prod.mk (a ^ c) (b ^ c) := rfl

Power Operation on Pair: $(a, b)^c = (a^c, b^c)$

Informal description

For any elements $a \in \alpha$, $b \in \beta$, and exponent $c \in E$, the power operation on the product type satisfies $(a, b)^c = (a^c, b^c)$.

Prod.pow_def theorem

(p : α × β) (c : E) : p ^ c = (p.1 ^ c, p.2 ^ c)

Full source

@[to_additive existing (reorder := 6 7) smul_def]
lemma pow_def (p : α × β) (c : E) : p ^ c = (p.1 ^ c, p.2 ^ c) := rfl

Component-wise Power Operation on Product Types

Informal description

For any pair $p = (a, b)$ in the product type $\alpha \times \beta$ and any exponent $c$ of type $E$, the power operation on the product is defined component-wise as $p^c = (a^c, b^c)$.

Prod.pow_swap theorem

(p : α × β) (c : E) : (p ^ c).swap = p.swap ^ c

Full source

@[to_additive existing (attr := simp) (reorder := 6 7) smul_swap]
lemma pow_swap (p : α × β) (c : E) : (p ^ c).swap = p.swap ^ c := rfl

Swapping Components Commutes with Exponentiation on Product Types

Informal description

For any pair $(x, y) \in \alpha \times \beta$ and any exponent $c \in E$, swapping the components of $(x, y)^c$ is equal to raising the swapped pair $(y, x)$ to the power $c$, i.e., $(x^c, y^c).\text{swap} = (y, x)^c$.