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.has_zero {I : Type u} {f : I → Type v} [Π (i : I), has_zero (f i)] :
has_zero (Π (i : I), f i)

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

Equations
@[simp]
theorem pi.zero_apply {I : Type u} {f : I → Type v} (i : I) [Π (i : I), has_zero (f i)] :
0 i = 0

@[simp]
theorem pi.one_apply {I : Type u} {f : I → Type v} (i : I) [Π (i : I), has_one (f i)] :
1 i = 1

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

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

@[simp]
theorem pi.add_apply {I : Type u} {f : I → Type v} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_add (f i)] :
(x + y) i = x i + y i

@[simp]
theorem pi.mul_apply {I : Type u} {f : I → Type v} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_mul (f i)] :
(x * y) i = (x i) * y i

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

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

@[simp]
theorem pi.neg_apply {I : Type u} {f : I → Type v} (x : Π (i : I), f i) (i : I) [Π (i : I), has_neg (f i)] :
(-x) i = -x i

@[simp]
theorem pi.inv_apply {I : Type u} {f : I → Type v} (x : Π (i : I), f i) (i : I) [Π (i : I), has_inv (f i)] :
x⁻¹ i = (x i)⁻¹

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

Equations
@[simp]
theorem pi.div_apply {I : Type u} {f : I → Type v} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_div (f i)] :
(x / y) i = x i / y i

@[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.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
@[simp]
theorem pi.sub_apply {I : Type u} {f : I → Type v} (x y : Π (i : I), f i) (i : I) [Π (i : I), add_group (f i)] :
(x - y) i = x i - y i

@[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.ordered_cancel_add_comm_monoid {I : Type u} {f : I → Type v} [Π (i : I), ordered_cancel_add_comm_monoid (f i)] :

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

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

@[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 pi.single {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) (x : f i) (i_1 : I) :
f i_1

The function supported at i, with value x there.

Equations
  • pi.single i x = λ (i' : I), dite (i' = i) (λ (h : i' = i), eq.rec (λ (x : f i'), x) h x) (λ (h : ¬i' = i), 0)
@[simp]
theorem pi.single_eq_same {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) (x : f i) :
pi.single i x i = x

@[simp]
theorem pi.single_eq_of_ne {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), has_zero (f i)] {i i' : I} (h : i' i) (x : f i) :
pi.single i x i' = 0

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 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) :