Mathlib.Algebra.GroupWithZero.Pi

Pi.mulZeroClass instance

: MulZeroClass (∀ i, α i)

Full source

instance mulZeroClass : MulZeroClass (∀ i, α i) where
  zero_mul := by intros; ext; exact zero_mul _
  mul_zero := by intros; ext; exact mul_zero _

Componentwise Multiplication and Zero on Product Types

Informal description

For a family of types $\alpha_i$ each equipped with a multiplication operation and a zero element, the product type $\forall i, \alpha_i$ inherits a `MulZeroClass` structure where multiplication and zero are defined componentwise.

MulHom.single definition

(i : ι) : α i →ₙ* ∀ i, α i

Full source

/-- The multiplicative homomorphism including a single `MulZeroClass`
into a dependent family of `MulZeroClass`es, as functions supported at a point.

This is the `MulHom` version of `Pi.single`. -/
@[simps]
def _root_.MulHom.single (i : ι) : α i →ₙ* ∀ i, α i where
  toFun := Pi.single i
  map_mul' := Pi.single_op₂ (fun _ ↦ (· * ·)) (fun _ ↦ zero_mul _) _

Multiplication-preserving single function

Informal description

For an index `i`, the function `MulHom.single i` maps an element `x` of `α i` to the function in the product type `∀ i, α i` that is `x` at index `i` and zero elsewhere. This function preserves multiplication, meaning that `MulHom.single i (x * y) = (MulHom.single i x) * (MulHom.single i y)` for any `x, y ∈ α i`.

Pi.single_mul theorem

(i : ι) (x y : α i) : single i (x * y) = single i x * single i y

Full source

lemma single_mul (i : ι) (x y : α i) : single i (x * y) = single i x * single i y :=
  (MulHom.single _).map_mul _ _

Single Function Preserves Multiplication: $\text{single}_i(x * y) = \text{single}_i(x) * \text{single}_i(y)$

Informal description

For any index $i$ in an index set $\iota$ and any elements $x, y$ in $\alpha_i$, the single function at index $i$ applied to the product $x * y$ is equal to the product of the single functions at index $i$ applied to $x$ and $y$ separately. In symbols: $$\text{single}_i(x * y) = \text{single}_i(x) * \text{single}_i(y).$$

Pi.single_mul_left_apply theorem

(i j : ι) (a : α i) (f : ∀ i, α i) : single i (a * f i) j = single i a j * f j

Full source

lemma single_mul_left_apply (i j : ι) (a : α i) (f : ∀ i, α i) :
    single i (a * f i) j = single i a j * f j :=
  (apply_single (fun i ↦ (· * f i)) (fun _ ↦ zero_mul _) _ _ _).symm

Single Function Multiplication Left Apply Identity

Informal description

For any indices $i, j$ in an index set $\iota$, an element $a$ in $\alpha_i$, and a function $f$ from $\iota$ to $\alpha_i$, the value of the single function at index $j$ applied to $a \cdot f(i)$ is equal to the product of the value of the single function at index $j$ applied to $a$ and the value of $f$ at $j$. In symbols: $$\text{single}_i(a \cdot f(i))_j = \text{single}_i(a)_j \cdot f(j).$$

Pi.single_mul_right_apply theorem

(i j : ι) (f : ∀ i, α i) (a : α i) : single i (f i * a) j = f j * single i a j

Full source

lemma single_mul_right_apply (i j : ι) (f : ∀ i, α i) (a : α i) :
    single i (f i * a) j = f j * single i a j :=
  (apply_single (f · * ·) (fun _ ↦ mul_zero _) _ _ _).symm

Single Function Multiplication Right Apply Identity

Informal description

For any indices $i, j$ in an index set $\iota$, a function $f$ from $\iota$ to $\alpha_i$, and an element $a$ in $\alpha_i$, the value of the single function at index $j$ applied to $f(i) \cdot a$ is equal to the product of $f(j)$ and the value of the single function at index $j$ applied to $a$. In symbols: $$\text{single}_i(f(i) \cdot a)_j = f(j) \cdot \text{single}_i(a)_j.$$

Pi.single_mul_left theorem

(a : α i) : single i (a * f i) = single i a * f

Full source

lemma single_mul_left (a : α i) : single i (a * f i) = single i a * f :=
  funext fun _ ↦ single_mul_left_apply _ _ _ _

Left Multiplication Identity for Single Function in Product Types

Informal description

For any index $i$ in an index set $\iota$, an element $a$ in $\alpha_i$, and a function $f$ from $\iota$ to $\alpha_i$, the single function applied to $a \cdot f(i)$ equals the product of the single function applied to $a$ and the function $f$. In symbols: $$\text{single}_i(a \cdot f(i)) = \text{single}_i(a) \cdot f.$$

Pi.single_mul_right theorem

(a : α i) : single i (f i * a) = f * single i a

Full source

lemma single_mul_right (a : α i) : single i (f i * a) = f * single i a :=
  funext fun _ ↦ single_mul_right_apply _ _ _ _

Right Multiplication Property of Single Function in Product Types

Informal description

For any element $a$ in $\alpha_i$, the single function at index $i$ applied to $f(i) \cdot a$ is equal to the product of the function $f$ and the single function at index $i$ applied to $a$. In symbols: $$\text{single}_i(f(i) \cdot a) = f \cdot \text{single}_i(a).$$

Pi.mulZeroOneClass instance

[∀ i, MulZeroOneClass (α i)] : MulZeroOneClass (∀ i, α i)

Full source

instance mulZeroOneClass [∀ i, MulZeroOneClass (α i)] : MulZeroOneClass (∀ i, α i) where
  __ := mulZeroClass
  __ := mulOneClass

Componentwise `MulZeroOneClass` Structure on Product Types

Informal description

For any family of types $(\alpha_i)_{i \in I}$ where each $\alpha_i$ is equipped with a multiplication operation, a multiplicative identity, and a zero element (i.e., each $\alpha_i$ is a `MulZeroOneClass`), the product type $\prod_{i \in I} \alpha_i$ inherits a `MulZeroOneClass` structure with pointwise multiplication, identity, and zero.

Pi.monoidWithZero instance

[∀ i, MonoidWithZero (α i)] : MonoidWithZero (∀ i, α i)

Full source

instance monoidWithZero [∀ i, MonoidWithZero (α i)] : MonoidWithZero (∀ i, α i) where
  __ := monoid
  __ := mulZeroClass

Componentwise Monoid with Zero Structure on Product Types

Informal description

For any family of types $(\alpha_i)_{i \in I}$ where each $\alpha_i$ is a monoid with zero, the product type $\prod_{i \in I} \alpha_i$ is also a monoid with zero, with multiplication and zero defined componentwise.

Pi.commMonoidWithZero instance

[∀ i, CommMonoidWithZero (α i)] : CommMonoidWithZero (∀ i, α i)

Full source

instance commMonoidWithZero [∀ i, CommMonoidWithZero (α i)] : CommMonoidWithZero (∀ i, α i) where
  __ := monoidWithZero
  __ := commMonoid

Componentwise Commutative Monoid with Zero Structure on Product Types

Informal description

For any family of types $(\alpha_i)_{i \in I}$ where each $\alpha_i$ is a commutative monoid with zero, the product type $\prod_{i \in I} \alpha_i$ is also a commutative monoid with zero, with multiplication and zero defined componentwise.

Pi.semigroupWithZero instance

[∀ i, SemigroupWithZero (α i)] : SemigroupWithZero (∀ i, α i)

Full source

instance semigroupWithZero [∀ i, SemigroupWithZero (α i)] : SemigroupWithZero (∀ i, α i) where
  __ := semigroup
  __ := mulZeroClass

Componentwise Semigroup with Zero Structure on Product Types

Informal description

For any family of types $(\alpha_i)_{i \in I}$ where each $\alpha_i$ is a semigroup with zero, the product type $\prod_{i \in I} \alpha_i$ is also a semigroup with zero, with multiplication and zero defined componentwise.