Mathlib.Algebra.Notation.Pi

Pi.instOne instance

[∀ i, One <| f i] : One (∀ i : I, f i)

Full source

@[to_additive]
instance instOne [∀ i, One <| f i] : One (∀ i : I, f i) :=
  ⟨fun _ => 1⟩

Pointwise Multiplicative Identity on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ has a multiplicative identity element $1$, the product type $\prod_{i \in I} f_i$ has a multiplicative identity defined pointwise as the function that maps each index $i$ to $1 \in f_i$.

Pi.one_apply theorem

[∀ i, One <| f i] : (1 : ∀ i, f i) i = 1

Full source

@[to_additive (attr := simp high)]
theorem one_apply [∀ i, One <| f i] : (1 : ∀ i, f i) i = 1 :=
  rfl

Componentwise Evaluation of Multiplicative Identity in Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ has a multiplicative identity element $1$, the $i$-th component of the multiplicative identity in the product type $\prod_{i \in I} f_i$ is equal to $1 \in f_i$.

Pi.one_def theorem

[∀ i, One <| f i] : (1 : ∀ i, f i) = fun _ => 1

Full source

@[to_additive]
theorem one_def [∀ i, One <| f i] : (1 : ∀ i, f i) = fun _ => 1 :=
  rfl

Definition of Pointwise Multiplicative Identity on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ has a multiplicative identity element $1$, the multiplicative identity in the product type $\prod_{i \in I} f_i$ is the constant function that maps every index $i$ to $1 \in f_i$.

Function.const_one theorem

[One β] : const α (1 : β) = 1

Full source

@[to_additive (attr := simp)] lemma _root_.Function.const_one [One β] : const α (1 : β) = 1 := rfl

Constant One Function Equals Multiplicative Identity in Function Space

Informal description

For any type $\beta$ with a multiplicative identity element $1$, the constant function from any type $\alpha$ to $\beta$ that maps every element to $1$ is equal to the multiplicative identity in the function space $\alpha \to \beta$.

Pi.one_comp theorem

[One γ] (x : α → β) : (1 : β → γ) ∘ x = 1

Full source

@[to_additive (attr := simp)]
theorem one_comp [One γ] (x : α → β) : (1 : β → γ) ∘ x = 1 :=
  rfl

Composition with Constant One Function Yields Constant One Function

Informal description

For any type $\gamma$ with a multiplicative identity element $1$, and any function $x : \alpha \to \beta$, the composition of the constant function $1 : \beta \to \gamma$ with $x$ equals the constant function $1 : \alpha \to \gamma$. In symbols: $$ (1_{\beta \to \gamma}) \circ x = 1_{\alpha \to \gamma} $$

Pi.comp_one theorem

[One β] (x : β → γ) : x ∘ (1 : α → β) = const α (x 1)

Full source

@[to_additive (attr := simp)]
theorem comp_one [One β] (x : β → γ) : x ∘ (1 : α → β) = const α (x 1) :=
  rfl

Composition with Constant One Function Yields Constant $x(1)$ Function

Informal description

For any type $\beta$ with a multiplicative identity element $1$, and any function $x : \beta \to \gamma$, the composition of $x$ with the constant function $1 : \alpha \to \beta$ equals the constant function from $\alpha$ to $\gamma$ that maps every element to $x(1)$. In symbols: $$ x \circ (1 : \alpha \to \beta) = \text{const}_\alpha (x(1)) $$

Pi.instMul instance

[∀ i, Mul <| f i] : Mul (∀ i : I, f i)

Full source

@[to_additive]
instance instMul [∀ i, Mul <| f i] : Mul (∀ i : I, f i) :=
  ⟨fun f g i => f i * g i⟩

Pointwise Multiplication on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a multiplication operation, the product type $\prod_{i \in I} f_i$ inherits a pointwise multiplication operation defined by $(x \cdot y)(i) = x(i) \cdot y(i)$ for all $i \in I$.

Pi.mul_apply theorem

[∀ i, Mul <| f i] : (x * y) i = x i * y i

Full source

@[to_additive (attr := simp)]
theorem mul_apply [∀ i, Mul <| f i] : (x * y) i = x i * y i :=
  rfl

Pointwise Multiplication Formula for Product Types: $(x \cdot y)(i) = x(i) \cdot y(i)$

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a multiplication operation, and for any elements $x, y \in \prod_{i \in I} f_i$, the $i$-th component of their product satisfies $(x \cdot y)(i) = x(i) \cdot y(i)$ for all $i \in I$.

Pi.mul_def theorem

[∀ i, Mul <| f i] : x * y = fun i => x i * y i

Full source

@[to_additive]
theorem mul_def [∀ i, Mul <| f i] : x * y = fun i => x i * y i :=
  rfl

Definition of Pointwise Multiplication on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a multiplication operation, the pointwise multiplication of two functions $x, y \in \prod_{i \in I} f_i$ is defined by $(x \cdot y)(i) = x(i) \cdot y(i)$ for all $i \in I$. In other words, $x \cdot y$ is the function that maps each index $i$ to the product $x(i) \cdot y(i)$.

Function.const_mul theorem

[Mul β] (a b : β) : const α a * const α b = const α (a * b)

Full source

@[to_additive (attr := simp)]
lemma _root_.Function.const_mul [Mul β] (a b : β) : const α a * const α b = const α (a * b) := rfl

Pointwise Multiplication of Constant Functions

Informal description

For any type $\alpha$ and any multiplicative type $\beta$, the pointwise product of two constant functions $\text{const}_\alpha a$ and $\text{const}_\alpha b$ is equal to the constant function $\text{const}_\alpha (a \cdot b)$, where $a, b \in \beta$.

Pi.mul_comp theorem

[Mul γ] (x y : β → γ) (z : α → β) : (x * y) ∘ z = x ∘ z * y ∘ z

Full source

@[to_additive]
theorem mul_comp [Mul γ] (x y : β → γ) (z : α → β) : (x * y) ∘ z = x ∘ z * y ∘ z :=
  rfl

Composition Distributes Over Pointwise Multiplication of Functions

Informal description

For any type $\gamma$ with a multiplication operation, and for any functions $x, y : \beta \to \gamma$ and $z : \alpha \to \beta$, the composition of the pointwise product $x * y$ with $z$ is equal to the pointwise product of the compositions $x \circ z$ and $y \circ z$. That is, $(x * y) \circ z = (x \circ z) * (y \circ z)$.

Pi.instSMul instance

[∀ i, SMul α <| f i] : SMul α (∀ i : I, f i)

Full source

@[to_additive]
instance instSMul [∀ i, SMul α <| f i] : SMul α (∀ i : I, f i) :=
  ⟨fun s x => fun i => s • x i⟩

Pointwise Scalar Multiplication on Product Types

Informal description

For any index type $I$ and family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a scalar multiplication operation by elements of type $\alpha$, the product type $\prod_{i \in I} f_i$ inherits a pointwise scalar multiplication operation defined by $(a \cdot x)_i = a \cdot x_i$ for each $a \in \alpha$, $x \in \prod_{i \in I} f_i$, and $i \in I$.

Pi.instPow instance

[∀ i, Pow (f i) β] : Pow (∀ i, f i) β

Full source

@[to_additive existing instSMul]
instance instPow [∀ i, Pow (f i) β] : Pow (∀ i, f i) β :=
  ⟨fun x b i => x i ^ b⟩

Pointwise Power Operation on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a power operation $\cdot^\beta$ for some fixed type $\beta$, the product type $\prod_{i \in I} f_i$ inherits a pointwise power operation defined by $(x^\beta)_i = x_i^\beta$ for each $x \in \prod_{i \in I} f_i$ and $i \in I$.

Pi.pow_apply theorem

[∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) (i : I) : (x ^ b) i = x i ^ b

Full source

@[to_additive (attr := simp, to_additive) (reorder := 5 6) smul_apply]
theorem pow_apply [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) (i : I) : (x ^ b) i = x i ^ b :=
  rfl

Pointwise Power Operation on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a power operation $\cdot^\beta$ for some fixed type $\beta$, and for any element $x \in \prod_{i \in I} f_i$ and any $b \in \beta$, the $i$-th component of the pointwise power $x^b$ equals the power of the $i$-th component of $x$, i.e., $(x^b)_i = x_i^b$ for all $i \in I$.

Pi.pow_def theorem

[∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) : x ^ b = fun i => x i ^ b

Full source

@[to_additive (attr := to_additive) (reorder := 5 6) smul_def]
theorem pow_def [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) : x ^ b = fun i => x i ^ b :=
  rfl

Definition of Pointwise Power Operation on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a power operation $\cdot^\beta$ for some fixed type $\beta$, and for any element $x \in \prod_{i \in I} f_i$ and exponent $b \in \beta$, the pointwise power operation is defined by $(x^b)_i = x_i^b$ for each $i \in I$. In other words, $x^b = \lambda i, x_i^b$.

Function.const_pow theorem

[Pow α β] (a : α) (b : β) : const I a ^ b = const I (a ^ b)

Full source

@[to_additive (attr := simp, to_additive) (reorder := 2 3, 5 6) smul_const]
lemma _root_.Function.const_pow [Pow α β] (a : α) (b : β) : const I a ^ b = const I (a ^ b) := rfl

Power of Constant Function Equals Constant of Power

Informal description

For any type $\alpha$ with a power operation $\cdot^\beta$, and for any element $a \in \alpha$ and exponent $b \in \beta$, the constant function $\text{const}_I a$ raised to the power $b$ is equal to the constant function $\text{const}_I (a^b)$.

Pi.pow_comp theorem

[Pow γ α] (x : β → γ) (a : α) (y : I → β) : (x ^ a) ∘ y = x ∘ y ^ a

Full source

@[to_additive (attr := to_additive) (reorder := 6 7) smul_comp]
theorem pow_comp [Pow γ α] (x : β → γ) (a : α) (y : I → β) : (x ^ a) ∘ y = x ∘ y ^ a :=
  rfl

Composition of Power Functions on Product Types

Informal description

For any type $\gamma$ equipped with a power operation $\cdot^\alpha$, any function $x : \beta \to \gamma$, any exponent $a : \alpha$, and any function $y : I \to \beta$, the composition of the power function $x^a$ with $y$ is equal to the composition of $x$ with the power function $y^a$. In symbols: $$(x^a) \circ y = x \circ (y^a).$$

Pi.instInv instance

[∀ i, Inv <| f i] : Inv (∀ i : I, f i)

Full source

@[to_additive]
instance instInv [∀ i, Inv <| f i] : Inv (∀ i : I, f i) :=
  ⟨fun f i => (f i)⁻¹⟩

Pointwise Inversion on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with an inversion operation, the product type $\prod_{i \in I} f_i$ inherits a pointwise inversion operation defined by $(x^{-1})_i = (x_i)^{-1}$ for each $x \in \prod_{i \in I} f_i$ and $i \in I$.

Pi.inv_apply theorem

[∀ i, Inv <| f i] : x⁻¹ i = (x i)⁻¹

Full source

@[to_additive (attr := simp)]
theorem inv_apply [∀ i, Inv <| f i] : x⁻¹ i = (x i)⁻¹ :=
  rfl

Componentwise Inversion Formula for Product Types: $(x^{-1})_i = (x_i)^{-1}$

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with an inversion operation, and for any element $x$ in the product type $\prod_{i \in I} f_i$, the $i$-th component of the inverse $x^{-1}$ is equal to the inverse of the $i$-th component of $x$. In symbols: $$(x^{-1})_i = (x_i)^{-1} \text{ for all } i \in I.$$

Pi.inv_def theorem

[∀ i, Inv <| f i] : x⁻¹ = fun i => (x i)⁻¹

Full source

@[to_additive]
theorem inv_def [∀ i, Inv <| f i] : x⁻¹ = fun i => (x i)⁻¹ :=
  rfl

Componentwise Inversion in Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with an inversion operation, the pointwise inversion of an element $x \in \prod_{i \in I} f_i$ is defined by $(x^{-1})_i = (x_i)^{-1}$ for each $i \in I$. In other words, the inversion operation on the product type is given componentwise by the inversion operations on each factor.

Function.const_inv theorem

[Inv β] (a : β) : (const α a)⁻¹ = const α a⁻¹

Full source

@[to_additive]
lemma _root_.Function.const_inv [Inv β] (a : β) : (const α a)⁻¹ = const α a⁻¹ := rfl

Inversion of Constant Function: $(\text{const}_\alpha a)^{-1} = \text{const}_\alpha (a^{-1})$

Informal description

For any type $\beta$ equipped with an inversion operation and any element $a \in \beta$, the pointwise inversion of the constant function $\text{const}_\alpha a$ (which maps every element of $\alpha$ to $a$) is equal to the constant function $\text{const}_\alpha (a^{-1})$.

Pi.inv_comp theorem

[Inv γ] (x : β → γ) (y : α → β) : x⁻¹ ∘ y = (x ∘ y)⁻¹

Full source

@[to_additive]
theorem inv_comp [Inv γ] (x : β → γ) (y : α → β) : x⁻¹x⁻¹ ∘ y = (x ∘ y)⁻¹ :=
  rfl

Inversion Commutes with Function Composition: $(x^{-1}) \circ y = (x \circ y)^{-1}$

Informal description

For any type $\gamma$ equipped with an inversion operation and any functions $x : \beta \to \gamma$ and $y : \alpha \to \beta$, the composition of the inversion of $x$ with $y$ equals the inversion of the composition of $x$ with $y$, i.e., $(x^{-1}) \circ y = (x \circ y)^{-1}$.

Pi.instDiv instance

[∀ i, Div <| f i] : Div (∀ i : I, f i)

Full source

@[to_additive]
instance instDiv [∀ i, Div <| f i] : Div (∀ i : I, f i) :=
  ⟨fun f g i => f i / g i⟩

Pointwise Division on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ has a division operation, the product type $\prod_{i \in I} f_i$ inherits a pointwise division operation defined by $(x / y)(i) = x(i) / y(i)$ for all $i \in I$.

Pi.div_apply theorem

[∀ i, Div <| f i] : (x / y) i = x i / y i

Full source

@[to_additive (attr := simp)]
theorem div_apply [∀ i, Div <| f i] : (x / y) i = x i / y i :=
  rfl

Pointwise Division Component Formula: $(x / y)(i) = x(i) / y(i)$

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ has a division operation, and for any elements $x, y$ in the product type $\prod_{i \in I} f_i$, the $i$-th component of the pointwise division $x / y$ is equal to the division of the $i$-th components of $x$ and $y$, i.e., $(x / y)(i) = x(i) / y(i)$.

Pi.div_def theorem

[∀ i, Div <| f i] : x / y = fun i => x i / y i

Full source

@[to_additive]
theorem div_def [∀ i, Div <| f i] : x / y = fun i => x i / y i :=
  rfl

Definition of Pointwise Division on Function Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ has a division operation, the pointwise division of two functions $x, y \colon \prod_{i \in I} f_i$ is defined by $(x / y)(i) = x(i) / y(i)$ for all $i \in I$.

Pi.div_comp theorem

[Div γ] (x y : β → γ) (z : α → β) : (x / y) ∘ z = x ∘ z / y ∘ z

Full source

@[to_additive]
theorem div_comp [Div γ] (x y : β → γ) (z : α → β) : (x / y) ∘ z = x ∘ z / y ∘ z :=
  rfl

Composition Preserves Pointwise Division

Informal description

For any type $\gamma$ with a division operation and functions $x, y : \beta \to \gamma$, and $z : \alpha \to \beta$, the composition of the pointwise division $(x / y)$ with $z$ is equal to the pointwise division of the compositions $x \circ z$ and $y \circ z$. That is, $(x / y) \circ z = (x \circ z) / (y \circ z)$.

Function.const_div theorem

[Div β] (a b : β) : const α a / const α b = const α (a / b)

Full source

@[to_additive (attr := simp)]
lemma _root_.Function.const_div [Div β] (a b : β) : const α a / const α b = const α (a / b) := rfl

Pointwise Division of Constant Functions: $\text{const}_\alpha a / \text{const}_\alpha b = \text{const}_\alpha (a / b)$

Informal description

For any type $\alpha$ and any type $\beta$ equipped with a division operation, the pointwise division of two constant functions $\text{const}_\alpha a$ and $\text{const}_\alpha b$ is equal to the constant function $\text{const}_\alpha (a / b)$. In other words, for any $a, b \in \beta$, we have $(\text{const}_\alpha a / \text{const}_\alpha b)(x) = \text{const}_\alpha (a / b)(x)$ for all $x \in \alpha$.