mathlib docs: algebra.group.pi

source

@[instance]

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

has_zero (Π (i : I), f i)

source

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

pi.has_one = {one := λ (_x : I), 1}

source

@[simp]

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

0 i = 0

source

@[simp]

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

1 i = 1

source

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

pi.has_mul = {mul := λ (f_1 g : Π (i : I), f i) (i : I), (f_1 i) * g i}

source

@[instance]

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

has_add (Π (i : I), f i)

source

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

source

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

source

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

pi.has_inv = {inv := λ (f_1 : Π (i : I), f i) (i : I), (f_1 i)⁻¹}

source

@[instance]

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

has_neg (Π (i : I), f i)

source

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

source

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

source

@[instance]

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

add_semigroup (Π (i : I), f i)

source

@[instance]

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

semigroup (Π (i : I), f i)

Equations

pi.semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _}

source

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

pi.comm_semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_comm := _}

source

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

source

@[instance]

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

add_monoid (Π (i : I), f i)

source

@[instance]

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

monoid (Π (i : I), f i)

Equations

pi.monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _}

source

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

pi.comm_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, mul_comm := _}

source

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

source

@[instance]

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

add_group (Π (i : I), f i)

source

@[instance]

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

group (Π (i : I), f i)

Equations

pi.group = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, inv := has_inv.inv pi.has_inv, mul_left_inv := _}

source

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

source

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

source

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

pi.comm_group = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, inv := has_inv.inv pi.has_inv, mul_left_inv := _, mul_comm := _}

source

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

source

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

pi.left_cancel_semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_left_cancel := _}

source

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

pi.right_cancel_semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_right_cancel := _}

source

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

source

@[instance]

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

ordered_cancel_add_comm_monoid (Π (i : I), f i)

source

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

pi.ordered_cancel_comm_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, mul_comm := _, mul_left_cancel := _, mul_right_cancel := _, le := has_le.le (preorder.to_has_le (Π (i : I), f i)), lt := has_lt.lt (preorder.to_has_lt (Π (i : I), f i)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}

source

@[instance]

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

ordered_comm_group (Π (i : I), f i)

Equations

pi.ordered_comm_group = {mul := comm_group.mul pi.comm_group, mul_assoc := _, one := comm_group.one pi.comm_group, one_mul := _, mul_one := _, inv := comm_group.inv pi.comm_group, mul_left_inv := _, mul_comm := _, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}

source

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

source

@[simp]

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

function.const α 1 = 1

source

@[simp]

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

function.const α 0 = 0

source

@[simp]

theorem pi.comp_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] {f : β → γ} :

f ∘ 0 = function.const α (f 0)

source

@[simp]

theorem pi.comp_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_one β] {f : β → γ} :

f ∘ 1 = function.const α (f 1)

source

@[simp]

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

0 ∘ f = 0

source

@[simp]

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

1 ∘ f = 1

source

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)

source

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

source

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

source

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.

source

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

monoid_hom.apply f i = {to_fun := λ (g : Π (i : I), f i), g i, map_one' := _, map_mul' := _}

source

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

⇑(add_monoid_hom.apply f i) g = g i

source

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

⇑(monoid_hom.apply f i) g = g i

source

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

add_monoid_hom.single f i = {to_fun := λ (x : f i), pi.single i x, map_zero' := _, map_add' := _}

source

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

⇑(add_monoid_hom.single f i) x = pi.single i x

mathlib documentation

Pi instances for groups and monoids