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 = { toMul := Pi.instMul, toZero := Pi.instZero, zero_mul := ⋯, mul_zero := ⋯ }

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' := ⋯ }

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

Equations

• Pi.mulZeroOneClass = { toOne := MulOneClass.toOne, toMul := MulZeroClass.toMul, one_mul := ⋯, mul_one := ⋯, toZero := MulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

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

Equations

• Pi.monoidWithZero = { toMonoid := Pi.monoid, toZero := MulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

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

Equations

• Pi.commMonoidWithZero = { toMonoid := MonoidWithZero.toMonoid, mul_comm := ⋯, toZero := MonoidWithZero.toZero, zero_mul := ⋯, mul_zero := ⋯ }

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

Equations

• Pi.semigroupWithZero = { toSemigroup := Pi.semigroup, toZero := MulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }