Pi instances for groups with zero

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

instance Pi.mulZeroClass {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] : MulZeroClass ((i : ι) → α i)

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.

@[simp]

theorem MulHom.single_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] (i : ι) (x : α i) (j : ι) : (single i) x j = Pi.single i x j

theorem Pi.single_mul {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] (i : ι) (x y : α i) : single i (x * y) = single i x * single i y

theorem Pi.single_mul_left_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] (i j : ι) (a : α i) (f : (i : ι) → α i) : single i (a * f i) j = single i a j * f j

theorem Pi.single_mul_right_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] (i j : ι) (f : (i : ι) → α i) (a : α i) : single i (f i * a) j = f j * single i a j

theorem Pi.single_mul_left {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] {i : ι} {f : (i : ι) → α i} (a : α i) : single i (a * f i) = single i a * f

theorem Pi.single_mul_right {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] {i : ι} {f : (i : ι) → α i} (a : α i) : single i (f i * a) = f * single i a

instance Pi.mulZeroOneClass {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroOneClass (α i)] : MulZeroOneClass ((i : ι) → α i)

instance Pi.monoidWithZero {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MonoidWithZero (α i)] : MonoidWithZero ((i : ι) → α i)

instance Pi.commMonoidWithZero {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CommMonoidWithZero (α i)] : CommMonoidWithZero ((i : ι) → α i)

instance Pi.semigroupWithZero {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → SemigroupWithZero (α i)] : SemigroupWithZero ((i : ι) → α i)