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.

source
theorem set.preimage_one {α : Type u_1} {β : Type u_2} [has_one β] (s : set β) [decidable (1 ∈ s)] :
1 ⁻¹' s = ite (1 ∈ s) set.univ ∅
source
theorem set.preimage_zero {α : Type u_1} {β : Type u_2} [has_zero β] (s : set β) [decidable (0 ∈ s)] :
0 ⁻¹' s = ite (0 ∈ s) set.univ ∅
source
@[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
source
@[protected, instance]
def pi.semigroup {I : Type u} {f : I → Type v} [Π (i : I), semigroup (f i)] :
semigroup (Π (i : I), f i)
Equations
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[protected, instance]
def pi.monoid {I : Type u} {f : I → Type v} [Π (i : I), monoid (f i)] :
monoid (Π (i : I), f i)
Equations
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[protected, instance]
def pi.division_comm_monoid {I : Type u} {f : I → Type v} [Π (i : I), division_comm_monoid (f i)] :
division_comm_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.subtraction_comm_monoid {I : Type u} {f : I → Type v} [Π (i : I), subtraction_comm_monoid (f i)] :
subtraction_comm_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.add_group {I : Type u} {f : I → Type v} [Π (i : I), add_group (f i)] :
add_group (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.group {I : Type u} {f : I → Type v} [Π (i : I), group (f i)] :
group (Π (i : I), f i)
Equations
source
@[protected, 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)
Equations
source
@[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
source
@[protected, 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)
Equations
source
@[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
source
@[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
source
@[protected, 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)
Equations
source
@[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
source
@[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
source
@[protected, instance]
def pi.add_right_cancel_monoid {I : Type u} {f : I → Type v} [Π (i : I), add_right_cancel_monoid (f i)] :
add_right_cancel_monoid (Π (i : I), f i)
Equations
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
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)) :
function.injective ⇑(pi.add_hom g)
source
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)) :
function.injective ⇑(pi.mul_hom g)
source
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
source
@[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
source
@[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
source
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
source
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)) :
function.injective ⇑(pi.add_monoid_hom g)
source
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)) :
function.injective ⇑(pi.monoid_hom g)
source
@[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
source
@[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
source
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
source
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
source
def pi.const_mul_hom (α : Type u_1) (β : Type u_2) [has_mul β] :
β →ₙ* α → β

function.const as a mul_hom.

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

function.const as an add_hom.

Equations
source
@[simp]
theorem pi.const_add_hom_apply (α : Type u_1) (β : Type u_2) [has_add β] (a : β) (ᾰ : α) :
⇑(pi.const_add_hom α β) a ᾰ = function.const α a ᾰ
source
@[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 ᾰ
source
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
source
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
source
@[simp]
theorem mul_hom.coe_fn_apply (α : Type u_1) (β : Type u_2) [has_mul α] [comm_semigroup β] (g : α →ₙ* β) (ᾰ : α) :
⇑(mul_hom.coe_fn α β) g ᾰ = ⇑g ᾰ
source
@[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) ᾰ
source
@[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
source
@[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
source
@[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) ᾰ
source
@[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) :
⇑(pi.eval_add_monoid_hom f i) g = g i
source
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
source
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
source
@[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) :
⇑(pi.eval_monoid_hom f i) g = g i
source
def pi.const_add_monoid_hom (α : Type u_1) (β : Type u_2) [add_zero_class β] :
β →+ α → β

function.const as an add_monoid_hom.

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

function.const as a monoid_hom.

Equations
source
@[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 ᾰ
source
@[simp]
theorem pi.const_add_monoid_hom_apply (α : Type u_1) (β : Type u_2) [add_zero_class β] (a : β) (ᾰ : α) :
⇑(pi.const_add_monoid_hom α β) a ᾰ = function.const α a ᾰ
source
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
source
@[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 ᾰ
source
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
source
@[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 ᾰ
source
@[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
source
@[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) ᾰ
source
@[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) ᾰ
source
@[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
source
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
source
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
source
@[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) :
⇑(zero_hom.single f i) x = pi.single i x
source
@[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) :
⇑(one_hom.single f i) x = pi.mul_single i x
source
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
source
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
source
@[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) :
⇑(add_monoid_hom.single f i) x = pi.single i x
source
@[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) :
⇑(monoid_hom.single f i) x = pi.mul_single i x
source
@[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
source
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
source
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) :
pi.single i (x ⊔ y) = pi.single i x ⊔ pi.single i y
source
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) :
pi.mul_single i (x ⊔ y) = pi.mul_single i x ⊔ pi.mul_single i y
source
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) :
pi.mul_single i (x ⊓ y) = pi.mul_single i x ⊓ pi.mul_single i y
source
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) :
pi.single i (x ⊓ y) = pi.single i x ⊓ pi.single i y
source
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) :
pi.mul_single i (x * y) = pi.mul_single i x * pi.mul_single i y
source
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
source
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) :
pi.single i (-x) = -pi.single i x
source
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) :
pi.mul_single i x⁻¹ = (pi.mul_single i x)⁻¹
source
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) :
pi.mul_single i (x / y) = pi.mul_single i x / pi.mul_single i y
source
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
source
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
source
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
source
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
source
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
source
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
source
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

source
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

source
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.

source
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.

source
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
source
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) :
function.update g i x = g / pi.mul_single i (g i) * pi.mul_single i x
source
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
source
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
source
@[simp]
theorem function.update_zero {I : Type u} {f : I → Type v} [Π (i : I), has_zero (f i)] [decidable_eq I] (i : I) :
function.update 0 i 0 = 0
source
@[simp]
theorem function.update_one {I : Type u} {f : I → Type v} [Π (i : I), has_one (f i)] [decidable_eq I] (i : I) :
function.update 1 i 1 = 1
source
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₂
source
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₂
source
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) :
function.update f₁⁻¹ i x₁⁻¹ = (function.update f₁ i x₁)⁻¹
source
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₁
source
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₂
source
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₂
source
@[simp]
theorem function.const_eq_one {ι : Type u_1} {α : Type u_2} [has_one α] [nonempty ι] {a : α} :
function.const ι a = 1 ↔ a = 1
source
@[simp]
theorem function.const_eq_zero {ι : Type u_1} {α : Type u_2} [has_zero α] [nonempty ι] {a : α} :
function.const ι a = 0 ↔ a = 0
source
theorem function.const_ne_one {ι : Type u_1} {α : Type u_2} [has_one α] [nonempty ι] {a : α} :
function.const ι a ≠ 1 ↔ a ≠ 1
source
theorem function.const_ne_zero {ι : Type u_1} {α : Type u_2} [has_zero α] [nonempty ι] {a : α} :
function.const ι a ≠ 0 ↔ a ≠ 0
source
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₂
source
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₂
source
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₁)⁻¹
source
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₁
source
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₂
source
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₂
source
@[simp]
theorem function.extend_by_one.hom_apply {ι : Type u_1} {η : Type v} (R : Type w) (s : ι → η) [mul_one_class R] (f : ι → R) (ᾰ : η) :
⇑(function.extend_by_one.hom R s) f ᾰ = function.extend s f 1 ᾰ
source
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
source
@[simp]
theorem function.extend_by_zero.hom_apply {ι : Type u_1} {η : Type v} (R : Type w) (s : ι → η) [add_zero_class R] (f : ι → R) (ᾰ : η) :
⇑(function.extend_by_zero.hom R s) f ᾰ = function.extend s f 0 ᾰ
source
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
source
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)] :
monotone (pi.single i)
source
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)] :
monotone (pi.mul_single i)
source
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)] :
strict_mono (pi.single i)
source
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)] :
strict_mono (pi.mul_single i)