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)

Equations

• Pi.mulZeroClass = MulZeroClass.mk ⋯ ⋯

@[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

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

• MulHom.single i = { toFun := Pi.single i, map_mul' := ⋯ }

theorem Pi.single_mul {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MulZeroClass (α i)] [DecidableEq ι] (i : ι) (x : α i) (y : α i) : Pi.single i (x * y) = Pi.single i x * Pi.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) : Pi.single i (a * f i) j = Pi.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) : Pi.single i (f i * a) j = f j * Pi.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) : Pi.single i (a * f i) = Pi.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) : Pi.single i (f i * a) = f * Pi.single i a

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

Equations

• Pi.mulZeroOneClass = let __spread.0 := Pi.mulZeroClass; let __spread.1 := Pi.mulOneClass; MulZeroOneClass.mk ⋯ ⋯

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

Equations

• Pi.monoidWithZero = let __spread.0 := Pi.monoid; let __spread.1 := Pi.mulZeroClass; MonoidWithZero.mk ⋯ ⋯

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

Equations

• Pi.commMonoidWithZero = let __spread.0 := Pi.monoidWithZero; let __spread.1 := Pi.commMonoid; CommMonoidWithZero.mk ⋯ ⋯

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

Equations

• Pi.semigroupWithZero = let __spread.0 := Pi.semigroup; let __spread.1 := Pi.mulZeroClass; SemigroupWithZero.mk ⋯ ⋯