mathlib documentation

algebra.group.pi

Pi instances for groups and monoids

This file defines instances for group, monoid, semigroup and related structures on Pi types.

@[instance]
def pi.add_semigroup {I : Type u} {f : I → Type v} [Π (i : I), add_semigroup (f i)] :
add_semigroup (Π (i : I), f i)

@[instance]
def pi.semigroup {I : Type u} {f : I → Type v} [Π (i : I), semigroup (f i)] :
semigroup (Π (i : I), f i)

Equations
@[instance]
def pi.comm_semigroup {I : Type u} {f : I → Type v} [Π (i : I), comm_semigroup (f i)] :
comm_semigroup (Π (i : I), f i)

Equations
@[instance]
def pi.add_comm_semigroup {I : Type u} {f : I → Type v} [Π (i : I), add_comm_semigroup (f i)] :
add_comm_semigroup (Π (i : I), f i)

@[instance]
def pi.add_monoid {I : Type u} {f : I → Type v} [Π (i : I), add_monoid (f i)] :
add_monoid (Π (i : I), f i)

@[instance]
def pi.monoid {I : Type u} {f : I → Type v} [Π (i : I), monoid (f i)] :
monoid (Π (i : I), f i)

Equations
@[instance]
def pi.comm_monoid {I : Type u} {f : I → Type v} [Π (i : I), comm_monoid (f i)] :
comm_monoid (Π (i : I), f i)

Equations
@[instance]
def pi.add_comm_monoid {I : Type u} {f : I → Type v} [Π (i : I), add_comm_monoid (f i)] :
add_comm_monoid (Π (i : I), f i)

@[instance]
def pi.sub_neg_add_monoid {I : Type u} {f : I → Type v} [Π (i : I), sub_neg_monoid (f i)] :
sub_neg_monoid (Π (i : I), f i)

@[instance]
def pi.div_inv_monoid {I : Type u} {f : I → Type v} [Π (i : I), div_inv_monoid (f i)] :
div_inv_monoid (Π (i : I), f i)

Equations
@[instance]
def pi.add_group {I : Type u} {f : I → Type v} [Π (i : I), add_group (f i)] :
add_group (Π (i : I), f i)

@[instance]
def pi.group {I : Type u} {f : I → Type v} [Π (i : I), group (f i)] :
group (Π (i : I), f i)

Equations
@[instance]
def pi.add_comm_group {I : Type u} {f : I → Type v} [Π (i : I), add_comm_group (f i)] :
add_comm_group (Π (i : I), f i)

@[instance]
def pi.comm_group {I : Type u} {f : I → Type v} [Π (i : I), comm_group (f i)] :
comm_group (Π (i : I), f i)

Equations
@[instance]
def pi.add_left_cancel_semigroup {I : Type u} {f : I → Type v} [Π (i : I), add_left_cancel_semigroup (f i)] :
add_left_cancel_semigroup (Π (i : I), f i)

@[instance]
def pi.left_cancel_semigroup {I : Type u} {f : I → Type v} [Π (i : I), left_cancel_semigroup (f i)] :
left_cancel_semigroup (Π (i : I), f i)

Equations
@[instance]
def pi.right_cancel_semigroup {I : Type u} {f : I → Type v} [Π (i : I), right_cancel_semigroup (f i)] :
right_cancel_semigroup (Π (i : I), f i)

Equations
@[instance]
def pi.add_right_cancel_semigroup {I : Type u} {f : I → Type v} [Π (i : I), add_right_cancel_semigroup (f i)] :
add_right_cancel_semigroup (Π (i : I), f i)

@[instance]
def pi.mul_zero_class {I : Type u} {f : I → Type v} [Π (i : I), mul_zero_class (f i)] :
mul_zero_class (Π (i : I), f i)

Equations
@[instance]
def pi.comm_monoid_with_zero {I : Type u} {f : I → Type v} [Π (i : I), comm_monoid_with_zero (f i)] :
comm_monoid_with_zero (Π (i : I), f i)

Equations
@[simp]
theorem pi.const_one {α : Type u_1} {β : Type u_2} [has_one β] :

@[simp]
theorem pi.const_zero {α : Type u_1} {β : Type u_2} [has_zero β] :

@[simp]
theorem pi.comp_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] {f : β → γ} :
f 0 = function.const α (f 0)

@[simp]
theorem pi.comp_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_one β] {f : β → γ} :
f 1 = function.const α (f 1)

@[simp]
theorem pi.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] {f : α → β} :
0 f = 0

@[simp]
theorem pi.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_one γ] {f : α → β} :
1 f = 1

def add_monoid_hom.apply {I : Type u} (f : I → Type v) [Π (i : I), add_monoid (f i)] (i : I) :
(Π (i : I), f i) →+ f i

Evaluation of functions into an indexed collection of additive monoids at a point is an additive monoid homomorphism.

def monoid_hom.apply {I : Type u} (f : I → Type v) [Π (i : I), monoid (f i)] (i : I) :
(Π (i : I), f i) →* f i

Evaluation of functions into an indexed collection of monoids at a point is a monoid homomorphism.

Equations
@[simp]
theorem add_monoid_hom.apply_apply {I : Type u} (f : I → Type v) [Π (i : I), add_monoid (f i)] (i : I) (g : Π (i : I), f i) :

@[simp]
theorem monoid_hom.apply_apply {I : Type u} (f : I → Type v) [Π (i : I), monoid (f i)] (i : I) (g : Π (i : I), f i) :

def monoid_hom.coe_fn (α : Type u_1) (β : Type u_2) [monoid α] [comm_monoid β] :
→* β) →* α → β

Coercion of a monoid_hom into a function is itself a monoid_hom.

See also monoid_hom.eval.

Equations
@[simp]
theorem monoid_hom.coe_fn_apply (α : Type u_1) (β : Type u_2) [monoid α] [comm_monoid β] (g : α →* β) (ᾰ : α) :
(monoid_hom.coe_fn α β) g = g ᾰ

def add_monoid_hom.coe_fn (α : Type u_1) (β : Type u_2) [add_monoid α] [add_comm_monoid β] :
→+ β) →+ α → β

Coercion of an add_monoid_hom into a function is itself a add_monoid_hom.

See also add_monoid_hom.eval.

def add_monoid_hom.single {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), add_monoid (f i)] (i : I) :
f i →+ Π (i : I), f i

The additive monoid homomorphism including a single additive monoid into a dependent family of additive monoids, as functions supported at a point.

Equations
@[simp]
theorem add_monoid_hom.single_apply {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), add_monoid (f i)] {i : I} (x : f i) :