mathlib3 documentation

algebra.group.pi

Pi instances for groups and monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem set.preimage_one {α : Type u_1} {β : Type u_2} [has_one β] (s : set β) [decidable (1 s)] :
theorem set.preimage_zero {α : Type u_1} {β : Type u_2} [has_zero β] (s : set β) [decidable (0 s)] :
@[protected, instance]
def pi.add_semigroup {I : Type u} {f : I Type v} [Π (i : I), add_semigroup (f i)] :
add_semigroup (Π (i : I), f i)
Equations
@[protected, instance]
def pi.semigroup {I : Type u} {f : I Type v} [Π (i : I), semigroup (f i)] :
semigroup (Π (i : I), f i)
Equations
@[protected, instance]
def pi.semigroup_with_zero {I : Type u} {f : I Type v} [Π (i : I), semigroup_with_zero (f i)] :
semigroup_with_zero (Π (i : I), f i)
Equations
@[protected, 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
@[protected, 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)
Equations
@[protected, instance]
def pi.mul_one_class {I : Type u} {f : I Type v} [Π (i : I), mul_one_class (f i)] :
mul_one_class (Π (i : I), f i)
Equations
@[protected, instance]
def pi.add_zero_class {I : Type u} {f : I Type v} [Π (i : I), add_zero_class (f i)] :
add_zero_class (Π (i : I), f i)
Equations
@[protected, instance]
def pi.add_monoid {I : Type u} {f : I Type v} [Π (i : I), add_monoid (f i)] :
add_monoid (Π (i : I), f i)
Equations
@[protected, instance]
def pi.monoid {I : Type u} {f : I Type v} [Π (i : I), monoid (f i)] :
monoid (Π (i : I), f i)
Equations
@[protected, 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
@[protected, 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)
Equations
@[protected, 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
@[protected, instance]
def pi.sub_neg_monoid {I : Type u} {f : I Type v} [Π (i : I), sub_neg_monoid (f i)] :
sub_neg_monoid (Π (i : I), f i)
Equations
@[protected, instance]
def pi.has_involutive_neg {I : Type u} {f : I Type v} [Π (i : I), has_involutive_neg (f i)] :
has_involutive_neg (Π (i : I), f i)
Equations
@[protected, instance]
def pi.has_involutive_inv {I : Type u} {f : I Type v} [Π (i : I), has_involutive_inv (f i)] :
has_involutive_inv (Π (i : I), f i)
Equations
@[protected, instance]
def pi.division_monoid {I : Type u} {f : I Type v} [Π (i : I), division_monoid (f i)] :
division_monoid (Π (i : I), f i)
Equations
@[protected, instance]
def pi.subtraction_monoid {I : Type u} {f : I Type v} [Π (i : I), subtraction_monoid (f i)] :
subtraction_monoid (Π (i : I), f i)
Equations
@[protected, instance]
def pi.group {I : Type u} {f : I Type v} [Π (i : I), group (f i)] :
group (Π (i : I), f i)
Equations
@[protected, 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
@[protected, instance]
def pi.add_left_cancel_semigroup {I : Type u} {f : I Type v} [Π (i : I), add_left_cancel_semigroup (f i)] :
Equations
@[protected, 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
@[protected, 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
@[protected, instance]
def pi.add_right_cancel_semigroup {I : Type u} {f : I Type v} [Π (i : I), add_right_cancel_semigroup (f i)] :
Equations
@[protected, instance]
def pi.add_left_cancel_monoid {I : Type u} {f : I Type v} [Π (i : I), add_left_cancel_monoid (f i)] :
add_left_cancel_monoid (Π (i : I), f i)
Equations
@[protected, instance]
def pi.left_cancel_monoid {I : Type u} {f : I Type v} [Π (i : I), left_cancel_monoid (f i)] :
left_cancel_monoid (Π (i : I), f i)
Equations
@[protected, instance]
def pi.add_right_cancel_monoid {I : Type u} {f : I Type v} [Π (i : I), add_right_cancel_monoid (f i)] :
Equations
@[protected, instance]
def pi.right_cancel_monoid {I : Type u} {f : I Type v} [Π (i : I), right_cancel_monoid (f i)] :
right_cancel_monoid (Π (i : I), f i)
Equations
@[protected, instance]
def pi.add_cancel_monoid {I : Type u} {f : I Type v} [Π (i : I), add_cancel_monoid (f i)] :
add_cancel_monoid (Π (i : I), f i)
Equations
@[protected, instance]
def pi.cancel_monoid {I : Type u} {f : I Type v} [Π (i : I), cancel_monoid (f i)] :
cancel_monoid (Π (i : I), f i)
Equations
@[protected, instance]
def pi.cancel_comm_monoid {I : Type u} {f : I Type v} [Π (i : I), cancel_comm_monoid (f i)] :
cancel_comm_monoid (Π (i : I), f i)
Equations
@[protected, instance]
def pi.add_cancel_comm_monoid {I : Type u} {f : I Type v} [Π (i : I), add_cancel_comm_monoid (f i)] :
add_cancel_comm_monoid (Π (i : I), f i)
Equations
@[protected, 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
@[protected, instance]
def pi.mul_zero_one_class {I : Type u} {f : I Type v} [Π (i : I), mul_zero_one_class (f i)] :
mul_zero_one_class (Π (i : I), f i)
Equations
@[protected, instance]
def pi.monoid_with_zero {I : Type u} {f : I Type v} [Π (i : I), monoid_with_zero (f i)] :
monoid_with_zero (Π (i : I), f i)
Equations
@[protected, 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
theorem add_hom.coe_add {M : Type u_1} {N : Type u_2} {mM : has_add M} {mN : add_comm_semigroup N} (f g : add_hom M N) :
f + g = λ (x : M), f x + g x
theorem mul_hom.coe_mul {M : Type u_1} {N : Type u_2} {mM : has_mul M} {mN : comm_semigroup N} (f g : M →ₙ* N) :
f * g = λ (x : M), f x * g x
def pi.add_hom {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), has_add (f i)] [has_add γ] (g : Π (i : I), add_hom γ (f i)) :
add_hom γ (Π (i : I), f i)

A family of add_hom f a : γ → β a defines a add_hom pi.add_hom f : γ → Π a, β a given by pi.add_hom f x b = f b x.

Equations
def pi.mul_hom {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), has_mul (f i)] [has_mul γ] (g : Π (i : I), γ →ₙ* f i) :
γ →ₙ* Π (i : I), f i

A family of mul_hom f a : γ →ₙ* β a defines a mul_hom pi.mul_hom f : γ →ₙ* Π a, β a given by pi.mul_hom f x b = f b x.

Equations
@[simp]
theorem pi.add_hom_apply {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), has_add (f i)] [has_add γ] (g : Π (i : I), add_hom γ (f i)) (x : γ) (i : I) :
(pi.add_hom g) x i = (g i) x
@[simp]
theorem pi.mul_hom_apply {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), has_mul (f i)] [has_mul γ] (g : Π (i : I), γ →ₙ* f i) (x : γ) (i : I) :
(pi.mul_hom g) x i = (g i) x
theorem pi.add_hom_injective {I : Type u} {f : I Type v} {γ : Type w} [nonempty I] [Π (i : I), has_add (f i)] [has_add γ] (g : Π (i : I), add_hom γ (f i)) (hg : (i : I), function.injective (g i)) :
theorem pi.mul_hom_injective {I : Type u} {f : I Type v} {γ : Type w} [nonempty I] [Π (i : I), has_mul (f i)] [has_mul γ] (g : Π (i : I), γ →ₙ* f i) (hg : (i : I), function.injective (g i)) :
def pi.add_monoid_hom {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), add_zero_class (f i)] [add_zero_class γ] (g : Π (i : I), γ →+ f i) :
γ →+ Π (i : I), f i

A family of additive monoid homomorphisms f a : γ →+ β a defines a monoid homomorphism pi.add_monoid_hom f : γ →+ Π a, β a given by pi.add_monoid_hom f x b = f b x.

Equations
@[simp]
theorem pi.add_monoid_hom_apply {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), add_zero_class (f i)] [add_zero_class γ] (g : Π (i : I), γ →+ f i) (x : γ) (i : I) :
(pi.add_monoid_hom g) x i = (g i) x
@[simp]
theorem pi.monoid_hom_apply {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), mul_one_class (f i)] [mul_one_class γ] (g : Π (i : I), γ →* f i) (x : γ) (i : I) :
(pi.monoid_hom g) x i = (g i) x
def pi.monoid_hom {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), mul_one_class (f i)] [mul_one_class γ] (g : Π (i : I), γ →* f i) :
γ →* Π (i : I), f i

A family of monoid homomorphisms f a : γ →* β a defines a monoid homomorphism pi.monoid_mul_hom f : γ →* Π a, β a given by pi.monoid_mul_hom f x b = f b x.

Equations
theorem pi.add_monoid_hom_injective {I : Type u} {f : I Type v} {γ : Type w} [nonempty I] [Π (i : I), add_zero_class (f i)] [add_zero_class γ] (g : Π (i : I), γ →+ f i) (hg : (i : I), function.injective (g i)) :
theorem pi.monoid_hom_injective {I : Type u} {f : I Type v} {γ : Type w} [nonempty I] [Π (i : I), mul_one_class (f i)] [mul_one_class γ] (g : Π (i : I), γ →* f i) (hg : (i : I), function.injective (g i)) :
@[simp]
theorem pi.eval_mul_hom_apply {I : Type u} (f : I Type v) [Π (i : I), has_mul (f i)] (i : I) (g : Π (i : I), f i) :
(pi.eval_mul_hom f i) g = g i
@[simp]
theorem pi.eval_add_hom_apply {I : Type u} (f : I Type v) [Π (i : I), has_add (f i)] (i : I) (g : Π (i : I), f i) :
(pi.eval_add_hom f i) g = g i
def pi.eval_mul_hom {I : Type u} (f : I Type v) [Π (i : I), has_mul (f i)] (i : I) :
(Π (i : I), f i) →ₙ* f i

Evaluation of functions into an indexed collection of semigroups at a point is a semigroup homomorphism. This is function.eval i as a mul_hom.

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

Evaluation of functions into an indexed collection of additive semigroups at a point is an additive semigroup homomorphism. This is function.eval i as an add_hom.

Equations
def pi.const_mul_hom (α : Type u_1) (β : Type u_2) [has_mul β] :
β →ₙ* α β

function.const as a mul_hom.

Equations
@[simp]
theorem pi.const_mul_hom_apply (α : Type u_1) (β : Type u_2) [has_mul β] (a : β) (ᾰ : α) :
(pi.const_mul_hom α β) a = function.const α a
def pi.const_add_hom (α : Type u_1) (β : Type u_2) [has_add β] :
add_hom β β)

function.const as an add_hom.

Equations
@[simp]
theorem pi.const_add_hom_apply (α : Type u_1) (β : Type u_2) [has_add β] (a : β) (ᾰ : α) :
(pi.const_add_hom α β) a = function.const α a
@[simp]
theorem add_hom.coe_fn_apply (α : Type u_1) (β : Type u_2) [has_add α] [add_comm_semigroup β] (g : add_hom α β) (ᾰ : α) :
(add_hom.coe_fn α β) g = g ᾰ
def mul_hom.coe_fn (α : Type u_1) (β : Type u_2) [has_mul α] [comm_semigroup β] :
→ₙ* β) →ₙ* α β

Coercion of a mul_hom into a function is itself a mul_hom. See also mul_hom.eval.

Equations
def add_hom.coe_fn (α : Type u_1) (β : Type u_2) [has_add α] [add_comm_semigroup β] :
add_hom (add_hom α β) β)

Coercion of an add_hom into a function is itself a add_hom. See also add_hom.eval.

Equations
@[simp]
theorem mul_hom.coe_fn_apply (α : Type u_1) (β : Type u_2) [has_mul α] [comm_semigroup β] (g : α →ₙ* β) (ᾰ : α) :
(mul_hom.coe_fn α β) g = g ᾰ
@[simp]
theorem add_hom.comp_left_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : add_hom α β) (I : Type u_3) (h : I α) (ᾰ : I) :
(f.comp_left I) h = (f h)
@[protected]
def add_hom.comp_left {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : add_hom α β) (I : Type u_3) :
add_hom (I α) (I β)

Additive semigroup homomorphism between the function spaces I → α and I → β, induced by an additive semigroup homomorphism f between α and β

Equations
@[protected]
def mul_hom.comp_left {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : α →ₙ* β) (I : Type u_3) :
(I α) →ₙ* I β

Semigroup homomorphism between the function spaces I → α and I → β, induced by a semigroup homomorphism f between α and β.

Equations
@[simp]
theorem mul_hom.comp_left_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : α →ₙ* β) (I : Type u_3) (h : I α) (ᾰ : I) :
(f.comp_left I) h = (f h)
@[simp]
theorem pi.eval_add_monoid_hom_apply {I : Type u} (f : I Type v) [Π (i : I), add_zero_class (f i)] (i : I) (g : Π (i : I), f i) :
def pi.eval_add_monoid_hom {I : Type u} (f : I Type v) [Π (i : I), add_zero_class (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. This is function.eval i as an add_monoid_hom.

Equations
def pi.eval_monoid_hom {I : Type u} (f : I Type v) [Π (i : I), mul_one_class (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. This is function.eval i as a monoid_hom.

Equations
@[simp]
theorem pi.eval_monoid_hom_apply {I : Type u} (f : I Type v) [Π (i : I), mul_one_class (f i)] (i : I) (g : Π (i : I), f i) :
def pi.const_add_monoid_hom (α : Type u_1) (β : Type u_2) [add_zero_class β] :
β →+ α β

function.const as an add_monoid_hom.

Equations
def pi.const_monoid_hom (α : Type u_1) (β : Type u_2) [mul_one_class β] :
β →* α β

function.const as a monoid_hom.

Equations
@[simp]
theorem pi.const_monoid_hom_apply (α : Type u_1) (β : Type u_2) [mul_one_class β] (a : β) (ᾰ : α) :
(pi.const_monoid_hom α β) a = function.const α a
@[simp]
theorem pi.const_add_monoid_hom_apply (α : Type u_1) (β : Type u_2) [add_zero_class β] (a : β) (ᾰ : α) :
def monoid_hom.coe_fn (α : Type u_1) (β : Type u_2) [mul_one_class α] [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) [mul_one_class α] [comm_monoid β] (g : α →* β) (ᾰ : α) :
(monoid_hom.coe_fn α β) g = g ᾰ
def add_monoid_hom.coe_fn (α : Type u_1) (β : Type u_2) [add_zero_class α] [add_comm_monoid β] :
→+ β) →+ α β

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

See also add_monoid_hom.eval.

Equations
@[simp]
theorem add_monoid_hom.coe_fn_apply (α : Type u_1) (β : Type u_2) [add_zero_class α] [add_comm_monoid β] (g : α →+ β) (ᾰ : α) :
(add_monoid_hom.coe_fn α β) g = g ᾰ
@[protected]
def add_monoid_hom.comp_left {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] (f : α →+ β) (I : Type u_3) :
(I α) →+ I β

Additive monoid homomorphism between the function spaces I → α and I → β, induced by an additive monoid homomorphism f between α and β

Equations
@[simp]
theorem monoid_hom.comp_left_apply {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) (I : Type u_3) (h : I α) (ᾰ : I) :
(f.comp_left I) h = (f h)
@[simp]
theorem add_monoid_hom.comp_left_apply {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] (f : α →+ β) (I : Type u_3) (h : I α) (ᾰ : I) :
(f.comp_left I) h = (f h)
@[protected]
def monoid_hom.comp_left {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) (I : Type u_3) :
(I α) →* I β

Monoid homomorphism between the function spaces I → α and I → β, induced by a monoid homomorphism f between α and β.

Equations
def one_hom.single {I : Type u} (f : I Type v) [decidable_eq I] [Π (i : I), has_one (f i)] (i : I) :
one_hom (f i) (Π (i : I), f i)

The one-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.

This is the one_hom version of pi.mul_single.

Equations
def zero_hom.single {I : Type u} (f : I Type v) [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) :
zero_hom (f i) (Π (i : I), f i)

The zero-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.

This is the zero_hom version of pi.single.

Equations
@[simp]
theorem zero_hom.single_apply {I : Type u} (f : I Type v) [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) (x : f i) :
@[simp]
theorem one_hom.single_apply {I : Type u} (f : I Type v) [decidable_eq I] [Π (i : I), has_one (f i)] (i : I) (x : f i) :
def monoid_hom.single {I : Type u} (f : I Type v) [decidable_eq I] [Π (i : I), mul_one_class (f i)] (i : I) :
f i →* Π (i : I), f i

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

This is the monoid_hom version of pi.mul_single.

Equations
def add_monoid_hom.single {I : Type u} (f : I Type v) [decidable_eq I] [Π (i : I), add_zero_class (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.

This is the add_monoid_hom version of pi.single.

Equations
@[simp]
theorem add_monoid_hom.single_apply {I : Type u} (f : I Type v) [decidable_eq I] [Π (i : I), add_zero_class (f i)] (i : I) (x : f i) :
@[simp]
theorem monoid_hom.single_apply {I : Type u} (f : I Type v) [decidable_eq I] [Π (i : I), mul_one_class (f i)] (i : I) (x : f i) :
@[simp]
theorem mul_hom.single_apply {I : Type u} (f : I Type v) [decidable_eq I] [Π (i : I), mul_zero_class (f i)] (i : I) (x : f i) (i_1 : I) :
(mul_hom.single f i) x i_1 = pi.single i x i_1
def mul_hom.single {I : Type u} (f : I Type v) [decidable_eq I] [Π (i : I), mul_zero_class (f i)] (i : I) :
f i →ₙ* Π (i : I), f i

The multiplicative homomorphism including a single mul_zero_class into a dependent family of mul_zero_classes, as functions supported at a point.

This is the mul_hom version of pi.single.

Equations
theorem pi.single_sup {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), semilattice_sup (f i)] [Π (i : I), has_zero (f i)] (i : I) (x y : f i) :
theorem pi.mul_single_sup {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), semilattice_sup (f i)] [Π (i : I), has_one (f i)] (i : I) (x y : f i) :
theorem pi.mul_single_inf {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), semilattice_inf (f i)] [Π (i : I), has_one (f i)] (i : I) (x y : f i) :
theorem pi.single_inf {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), semilattice_inf (f i)] [Π (i : I), has_zero (f i)] (i : I) (x y : f i) :
theorem pi.mul_single_mul {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), mul_one_class (f i)] (i : I) (x y : f i) :
theorem pi.single_add {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), add_zero_class (f i)] (i : I) (x y : f i) :
pi.single i (x + y) = pi.single i x + pi.single i y
theorem pi.single_neg {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), add_group (f i)] (i : I) (x : f i) :
theorem pi.mul_single_inv {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), group (f i)] (i : I) (x : f i) :
theorem pi.single_div {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), group (f i)] (i : I) (x y : f i) :
theorem pi.single_sub {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), add_group (f i)] (i : I) (x y : f i) :
pi.single i (x - y) = pi.single i x - pi.single i y
theorem pi.single_mul {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), mul_zero_class (f i)] (i : I) (x y : f i) :
pi.single i (x * y) = pi.single i x * pi.single i y
theorem pi.single_mul_left_apply {I : Type u} {f : I Type v} (x : Π (i : I), f i) (i j : I) [decidable_eq I] [Π (i : I), mul_zero_class (f i)] (a : f i) :
pi.single i (a * x i) j = pi.single i a j * x j
theorem pi.single_mul_right_apply {I : Type u} {f : I Type v} (x : Π (i : I), f i) (i j : I) [decidable_eq I] [Π (i : I), mul_zero_class (f i)] (a : f i) :
pi.single i (x i * a) j = x j * pi.single i a j
theorem pi.single_mul_left {I : Type u} {f : I Type v} (x : Π (i : I), f i) (i : I) [decidable_eq I] [Π (i : I), mul_zero_class (f i)] (a : f i) :
pi.single i (a * x i) = pi.single i a * x
theorem pi.single_mul_right {I : Type u} {f : I Type v} (x : Π (i : I), f i) (i : I) [decidable_eq I] [Π (i : I), mul_zero_class (f i)] (a : f i) :
pi.single i (x i * a) = x * pi.single i a
theorem pi.mul_single_commute {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), mul_one_class (f i)] :
pairwise (λ (i j : I), (x : f i) (y : f j), commute (pi.mul_single i x) (pi.mul_single j y))

The injection into a pi group at different indices commutes.

For injections of commuting elements at the same index, see commute.map

theorem pi.single_commute {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), add_zero_class (f i)] :
pairwise (λ (i j : I), (x : f i) (y : f j), add_commute (pi.single i x) (pi.single j y))

The injection into an additive pi group at different indices commutes.

For injections of commuting elements at the same index, see add_commute.map

theorem pi.mul_single_apply_commute {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), mul_one_class (f i)] (x : Π (i : I), f i) (i j : I) :
commute (pi.mul_single i (x i)) (pi.mul_single j (x j))

The injection into a pi group with the same values commutes.

theorem pi.single_apply_commute {I : Type u} {f : I Type v} [decidable_eq I] [Π (i : I), add_zero_class (f i)] (x : Π (i : I), f i) (i j : I) :
add_commute (pi.single i (x i)) (pi.single j (x j))

The injection into an additive pi group with the same values commutes.

theorem pi.update_eq_sub_add_single {I : Type u} {f : I Type v} (i : I) [decidable_eq I] [Π (i : I), add_group (f i)] (g : Π (i : I), f i) (x : f i) :
function.update g i x = g - pi.single i (g i) + pi.single i x
theorem pi.update_eq_div_mul_single {I : Type u} {f : I Type v} (i : I) [decidable_eq I] [Π (i : I), group (f i)] (g : Π (i : I), f i) (x : f i) :
theorem pi.mul_single_mul_mul_single_eq_mul_single_mul_mul_single {I : Type u} [decidable_eq I] {M : Type u_1} [comm_monoid M] {k l m n : I} {u v : M} (hu : u 1) (hv : v 1) :
pi.mul_single k u * pi.mul_single l v = pi.mul_single m u * pi.mul_single n v k = m l = n u = v k = n l = m u * v = 1 k = l m = n
theorem pi.single_add_single_eq_single_add_single {I : Type u} [decidable_eq I] {M : Type u_1} [add_comm_monoid M] {k l m n : I} {u v : M} (hu : u 0) (hv : v 0) :
pi.single k u + pi.single l v = pi.single m u + pi.single n v k = m l = n u = v k = n l = m u + v = 0 k = l m = n
@[simp]
theorem function.update_zero {I : Type u} {f : I Type v} [Π (i : I), has_zero (f i)] [decidable_eq I] (i : I) :
@[simp]
theorem function.update_one {I : Type u} {f : I Type v} [Π (i : I), has_one (f i)] [decidable_eq I] (i : I) :
theorem function.update_add {I : Type u} {f : I Type v} [Π (i : I), has_add (f i)] [decidable_eq I] (f₁ f₂ : Π (i : I), f i) (i : I) (x₁ x₂ : f i) :
function.update (f₁ + f₂) i (x₁ + x₂) = function.update f₁ i x₁ + function.update f₂ i x₂
theorem function.update_mul {I : Type u} {f : I Type v} [Π (i : I), has_mul (f i)] [decidable_eq I] (f₁ f₂ : Π (i : I), f i) (i : I) (x₁ x₂ : f i) :
function.update (f₁ * f₂) i (x₁ * x₂) = function.update f₁ i x₁ * function.update f₂ i x₂
theorem function.update_inv {I : Type u} {f : I Type v} [Π (i : I), has_inv (f i)] [decidable_eq I] (f₁ : Π (i : I), f i) (i : I) (x₁ : f i) :
theorem function.update_neg {I : Type u} {f : I Type v} [Π (i : I), has_neg (f i)] [decidable_eq I] (f₁ : Π (i : I), f i) (i : I) (x₁ : f i) :
function.update (-f₁) i (-x₁) = -function.update f₁ i x₁
theorem function.update_sub {I : Type u} {f : I Type v} [Π (i : I), has_sub (f i)] [decidable_eq I] (f₁ f₂ : Π (i : I), f i) (i : I) (x₁ x₂ : f i) :
function.update (f₁ - f₂) i (x₁ - x₂) = function.update f₁ i x₁ - function.update f₂ i x₂
theorem function.update_div {I : Type u} {f : I Type v} [Π (i : I), has_div (f i)] [decidable_eq I] (f₁ f₂ : Π (i : I), f i) (i : I) (x₁ x₂ : f i) :
function.update (f₁ / f₂) i (x₁ / x₂) = function.update f₁ i x₁ / function.update f₂ i x₂
@[simp]
theorem function.const_eq_one {ι : Type u_1} {α : Type u_2} [has_one α] [nonempty ι] {a : α} :
function.const ι a = 1 a = 1
@[simp]
theorem function.const_eq_zero {ι : Type u_1} {α : Type u_2} [has_zero α] [nonempty ι] {a : α} :
function.const ι a = 0 a = 0
theorem function.const_ne_one {ι : Type u_1} {α : Type u_2} [has_one α] [nonempty ι] {a : α} :
theorem function.const_ne_zero {ι : Type u_1} {α : Type u_2} [has_zero α] [nonempty ι] {a : α} :
theorem set.piecewise_add {I : Type u} {f : I Type v} [Π (i : I), has_add (f i)] (s : set I) [Π (i : I), decidable (i s)] (f₁ f₂ g₁ g₂ : Π (i : I), f i) :
s.piecewise (f₁ + f₂) (g₁ + g₂) = s.piecewise f₁ g₁ + s.piecewise f₂ g₂
theorem set.piecewise_mul {I : Type u} {f : I Type v} [Π (i : I), has_mul (f i)] (s : set I) [Π (i : I), decidable (i s)] (f₁ f₂ g₁ g₂ : Π (i : I), f i) :
s.piecewise (f₁ * f₂) (g₁ * g₂) = s.piecewise f₁ g₁ * s.piecewise f₂ g₂
theorem set.piecewise_inv {I : Type u} {f : I Type v} [Π (i : I), has_inv (f i)] (s : set I) [Π (i : I), decidable (i s)] (f₁ g₁ : Π (i : I), f i) :
s.piecewise f₁⁻¹ g₁⁻¹ = (s.piecewise f₁ g₁)⁻¹
theorem set.piecewise_neg {I : Type u} {f : I Type v} [Π (i : I), has_neg (f i)] (s : set I) [Π (i : I), decidable (i s)] (f₁ g₁ : Π (i : I), f i) :
s.piecewise (-f₁) (-g₁) = -s.piecewise f₁ g₁
theorem set.piecewise_div {I : Type u} {f : I Type v} [Π (i : I), has_div (f i)] (s : set I) [Π (i : I), decidable (i s)] (f₁ f₂ g₁ g₂ : Π (i : I), f i) :
s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂
theorem set.piecewise_sub {I : Type u} {f : I Type v} [Π (i : I), has_sub (f i)] (s : set I) [Π (i : I), decidable (i s)] (f₁ f₂ g₁ g₂ : Π (i : I), f i) :
s.piecewise (f₁ - f₂) (g₁ - g₂) = s.piecewise f₁ g₁ - s.piecewise f₂ g₂
@[simp]
theorem function.extend_by_one.hom_apply {ι : Type u_1} {η : Type v} (R : Type w) (s : ι η) [mul_one_class R] (f : ι R) (ᾰ : η) :
noncomputable def function.extend_by_zero.hom {ι : Type u_1} {η : Type v} (R : Type w) (s : ι η) [add_zero_class R] :
R) →+ η R

function.extend s f 0 as a bundled hom.

Equations
@[simp]
theorem function.extend_by_zero.hom_apply {ι : Type u_1} {η : Type v} (R : Type w) (s : ι η) [add_zero_class R] (f : ι R) (ᾰ : η) :
noncomputable def function.extend_by_one.hom {ι : Type u_1} {η : Type v} (R : Type w) (s : ι η) [mul_one_class R] :
R) →* η R

function.extend s f 1 as a bundled hom.

Equations
theorem pi.single_mono {I : Type u} {f : I Type v} (i : I) [decidable_eq I] [Π (i : I), preorder (f i)] [Π (i : I), has_zero (f i)] :
theorem pi.mul_single_mono {I : Type u} {f : I Type v} (i : I) [decidable_eq I] [Π (i : I), preorder (f i)] [Π (i : I), has_one (f i)] :
theorem pi.single_strict_mono {I : Type u} {f : I Type v} (i : I) [decidable_eq I] [Π (i : I), preorder (f i)] [Π (i : I), has_zero (f i)] :
theorem pi.mul_single_strict_mono {I : Type u} {f : I Type v} (i : I) [decidable_eq I] [Π (i : I), preorder (f i)] [Π (i : I), has_one (f i)] :