Documentation

Mathlib.Algebra.GroupWithZero.Pi

Pi instances for groups with zero #

This file defines monoid with zero, group with zero, and related structure instances for pi types.

source
instance Pi.mulZeroClass {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] :
MulZeroClass ((i : ι) → α i)
Equations
source
def MulHom.single {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] (i : ι) :
α i →ₙ* (i : ι) → α i

The multiplicative homomorphism including a single MulZeroClass into a dependent family of MulZeroClasses, as functions supported at a point.

This is the MulHom version of Pi.single.

Equations
Instances For
    source
    @[simp]
    theorem MulHom.single_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] (i : ι) (x : α i) (j : ι) :
    (MulHom.single i) x j = Pi.single i x j
    source
    theorem Pi.single_mul {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] (i : ι) (x y : α i) :
    Pi.single i (x * y) = Pi.single i x * Pi.single i y
    source
    theorem Pi.single_mul_left_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] (i j : ι) (a : α i) (f : (i : ι) → α i) :
    Pi.single i (a * f i) j = Pi.single i a j * f j
    source
    theorem Pi.single_mul_right_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] (i j : ι) (f : (i : ι) → α i) (a : α i) :
    Pi.single i (f i * a) j = f j * Pi.single i a j
    source
    theorem Pi.single_mul_left {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] {i : ι} {f : (i : ι) → α i} (a : α i) :
    Pi.single i (a * f i) = Pi.single i a * f
    source
    theorem Pi.single_mul_right {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] {i : ι} {f : (i : ι) → α i} (a : α i) :
    Pi.single i (f i * a) = f * Pi.single i a
    source
    instance Pi.mulZeroOneClass {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroOneClass (α i)] :
    MulZeroOneClass ((i : ι) → α i)
    Equations
    source
    instance Pi.monoidWithZero {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MonoidWithZero (α i)] :
    MonoidWithZero ((i : ι) → α i)
    Equations
    source
    instance Pi.commMonoidWithZero {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CommMonoidWithZero (α i)] :
    CommMonoidWithZero ((i : ι) → α i)
    Equations
    source
    instance Pi.semigroupWithZero {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → SemigroupWithZero (α i)] :
    SemigroupWithZero ((i : ι) → α i)
    Equations