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.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
@[protected, instance]
def pi.subtraction_comm_monoid {I : Type u} {f : I Type v} [Π (i : I), ] :
Equations
@[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
@[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.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
@[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), ] :
Equations
@[protected, instance]
def pi.left_cancel_semigroup {I : Type u} {f : I Type v} [Π (i : 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 (Π (i : I), f i)
Equations
@[protected, instance]
def pi.add_right_cancel_semigroup {I : Type u} {f : I Type v} [Π (i : I), ] :
Equations
@[protected, instance]
def pi.add_left_cancel_monoid {I : Type u} {f : I Type v} [Π (i : 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), ] :
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 (Π (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 (Π (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 : 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), (f i)) :
(Π (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), (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), (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)] (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)] (g : Π (i : I), γ →+ f i) (x : γ) (i : I) :
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)] (g : Π (i : I), γ →* f i) (x : γ) (i : I) :
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)] (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)] (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)] (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) :
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) :
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 : β) (ᾰ : α) :
β) a =
def pi.const_add_hom (α : Type u_1) (β : Type u_2) [has_add β] :
β)

`function.const` as an `add_hom`.

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

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 α]  :

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 α] (g : α →ₙ* β) (ᾰ : α) :
β) g = g ᾰ
@[simp]
theorem add_hom.comp_left_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : β) (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 : β) (I : Type u_3) :

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) :
g = g 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) :
i) g = g i
def pi.const_add_monoid_hom (α : Type u_1) (β : Type u_2)  :
β →+ α β

`function.const` as an `add_monoid_hom`.

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

`function.const` as a `monoid_hom`.

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

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) (g : α →+ β) (ᾰ : α) :
g = g ᾰ
@[protected]
def add_monoid_hom.comp_left {α : Type u_1} {β : Type u_2} (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} (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} (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} (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) :
i) x = x
@[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) :
i) x =
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) :
x = x
@[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) :
i) x =
@[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) :
i) x i_1 = 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_class`es, as functions supported at a point.

This is the `mul_hom` version of `pi.single`.

Equations
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) :
(x * y) = *
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) :
(x + y) = x + 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) :
(-x) = - x
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) :
= x)⁻¹
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) :
(x / y) = /
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) :
(x - y) = x - 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) :
(x * y) = x * y
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 x) 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 x) 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 (x i)) (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) :

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) :
x = g - (g 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) :
x = g / (g 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) :
* = * 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} {k l m n : I} {u v : M} (hu : u 0) (hv : v 0) :
u + v = u + 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) :
0 = 0
@[simp]
theorem function.update_one {I : Type u} {f : I Type v} [Π (i : I), has_one (f i)] [decidable_eq I] (i : I) :
1 = 1
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₂) = i x₁ + 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₂) = i x₁ * 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) :
x₁⁻¹ = i x₁)⁻¹
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₁) = - 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₂) = i x₁ - 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₂) = i x₁ / i x₂
@[simp]
theorem function.const_eq_one {ι : Type u_1} {α : Type u_2} [has_one α] [nonempty ι] {a : α} :
= 1 a = 1
@[simp]
theorem function.const_eq_zero {ι : Type u_1} {α : Type u_2} [has_zero α] [nonempty ι] {a : α} :
= 0 a = 0
theorem function.const_ne_one {ι : Type u_1} {α : Type u_2} [has_one α] [nonempty ι] {a : α} :
1 a 1
theorem function.const_ne_zero {ι : Type u_1} {α : Type u_2} [has_zero α] [nonempty ι] {a : α} :
0 a 0
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 : ι η) (f : ι R) (ᾰ : η) :
f = 1
noncomputable def function.extend_by_zero.hom {ι : Type u_1} {η : Type v} (R : Type w) (s : ι η)  :
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 : ι η) (f : ι R) (ᾰ : η) :
f = 0
noncomputable def function.extend_by_one.hom {ι : Type u_1} {η : Type v} (R : Type w) (s : ι η)  :
R) →* η R

`function.extend s f 1` as a bundled hom.

Equations