mathlib3 documentation

group_theory.group_action.prod

Prod instances for additive and multiplicative actions #

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

This file defines instances for binary product of additive and multiplicative actions and provides scalar multiplication as a homomorphism from α × β to β.

Main declarations #

See also #

@[protected, instance]
def prod.has_vadd {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] :
has_vadd M × β)
Equations
@[protected, instance]
def prod.has_smul {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] :
has_smul M × β)
Equations
@[simp]
theorem prod.vadd_fst {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] (a : M) (x : α × β) :
(a +ᵥ x).fst = a +ᵥ x.fst
@[simp]
theorem prod.smul_fst {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] (a : M) (x : α × β) :
(a x).fst = a x.fst
@[simp]
theorem prod.smul_snd {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] (a : M) (x : α × β) :
(a x).snd = a x.snd
@[simp]
theorem prod.vadd_snd {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] (a : M) (x : α × β) :
(a +ᵥ x).snd = a +ᵥ x.snd
@[simp]
theorem prod.smul_mk {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] (a : M) (b : α) (c : β) :
a (b, c) = (a b, a c)
@[simp]
theorem prod.vadd_mk {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] (a : M) (b : α) (c : β) :
a +ᵥ (b, c) = (a +ᵥ b, a +ᵥ c)
theorem prod.vadd_def {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] (a : M) (x : α × β) :
a +ᵥ x = (a +ᵥ x.fst, a +ᵥ x.snd)
theorem prod.smul_def {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] (a : M) (x : α × β) :
a x = (a x.fst, a x.snd)
@[simp]
theorem prod.vadd_swap {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] (a : M) (x : α × β) :
(a +ᵥ x).swap = a +ᵥ x.swap
@[simp]
theorem prod.smul_swap {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] (a : M) (x : α × β) :
(a x).swap = a x.swap
theorem prod.smul_zero_mk {M : Type u_1} {β : Type u_6} [has_smul M β] {α : Type u_2} [monoid M] [add_monoid α] [distrib_mul_action M α] (a : M) (c : β) :
a (0, c) = (0, a c)
theorem prod.smul_mk_zero {M : Type u_1} {α : Type u_5} [has_smul M α] {β : Type u_2} [monoid M] [add_monoid β] [distrib_mul_action M β] (a : M) (b : α) :
a (b, 0) = (a b, 0)
@[protected, instance]
def prod.has_pow {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] :
has_pow × β) E
Equations
@[simp]
theorem prod.pow_fst {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] (p : α × β) (c : E) :
(p ^ c).fst = p.fst ^ c
@[simp]
theorem prod.pow_snd {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] (p : α × β) (c : E) :
(p ^ c).snd = p.snd ^ c
@[simp]
theorem prod.pow_mk {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] (c : E) (a : α) (b : β) :
(a, b) ^ c = (a ^ c, b ^ c)
theorem prod.pow_def {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] (p : α × β) (c : E) :
p ^ c = (p.fst ^ c, p.snd ^ c)
@[simp]
theorem prod.pow_swap {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] (p : α × β) (c : E) :
(p ^ c).swap = p.swap ^ c
@[protected, instance]
def prod.vadd_assoc_class {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] [has_vadd N α] [has_vadd N β] [has_vadd M N] [vadd_assoc_class M N α] [vadd_assoc_class M N β] :
vadd_assoc_class M N × β)
@[protected, instance]
def prod.is_scalar_tower {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] [has_smul N α] [has_smul N β] [has_smul M N] [is_scalar_tower M N α] [is_scalar_tower M N β] :
is_scalar_tower M N × β)
@[protected, instance]
def prod.vadd_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] [has_vadd N α] [has_vadd N β] [vadd_comm_class M N α] [vadd_comm_class M N β] :
vadd_comm_class M N × β)
@[protected, instance]
def prod.smul_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] [has_smul N α] [has_smul N β] [smul_comm_class M N α] [smul_comm_class M N β] :
smul_comm_class M N × β)
@[protected, instance]
def prod.is_central_vadd {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] [has_vadd Mᵃᵒᵖ α] [has_vadd Mᵃᵒᵖ β] [is_central_vadd M α] [is_central_vadd M β] :
@[protected, instance]
def prod.is_central_scalar {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] [has_smul Mᵐᵒᵖ α] [has_smul Mᵐᵒᵖ β] [is_central_scalar M α] [is_central_scalar M β] :
@[protected, instance]
def prod.has_faithful_vadd_left {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] [has_faithful_vadd M α] [nonempty β] :
@[protected, instance]
def prod.has_faithful_smul_left {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] [has_faithful_smul M α] [nonempty β] :
@[protected, instance]
def prod.has_faithful_vadd_right {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] [nonempty α] [has_faithful_vadd M β] :
@[protected, instance]
def prod.has_faithful_smul_right {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] [nonempty α] [has_faithful_smul M β] :
@[protected, instance]
def prod.vadd_comm_class_both {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add N] [has_add P] [has_vadd M N] [has_vadd M P] [vadd_comm_class M N N] [vadd_comm_class M P P] :
vadd_comm_class M (N × P) (N × P)
@[protected, instance]
def prod.smul_comm_class_both {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul N] [has_mul P] [has_smul M N] [has_smul M P] [smul_comm_class M N N] [smul_comm_class M P P] :
smul_comm_class M (N × P) (N × P)
@[protected, instance]
def prod.is_scalar_tower_both {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul N] [has_mul P] [has_smul M N] [has_smul M P] [is_scalar_tower M N N] [is_scalar_tower M P P] :
is_scalar_tower M (N × P) (N × P)
@[protected, instance]
def prod.add_action {M : Type u_1} {α : Type u_5} {β : Type u_6} {m : add_monoid M} [add_action M α] [add_action M β] :
add_action M × β)
Equations
@[protected, instance]
def prod.mul_action {M : Type u_1} {α : Type u_5} {β : Type u_6} {m : monoid M} [mul_action M α] [mul_action M β] :
mul_action M × β)
Equations
@[protected, instance]
def prod.smul_zero_class {R : Type u_1} {M : Type u_2} {N : Type u_3} [has_zero M] [has_zero N] [smul_zero_class R M] [smul_zero_class R N] :
Equations

Scalar multiplication as a homomorphism #

@[simp]
theorem smul_mul_hom_apply {α : Type u_5} {β : Type u_6} [monoid α] [has_mul β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] (a : α × β) :
def smul_mul_hom {α : Type u_5} {β : Type u_6} [monoid α] [has_mul β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] :
α × β →ₙ* β

Scalar multiplication as a multiplicative homomorphism.

Equations
def smul_monoid_hom {α : Type u_5} {β : Type u_6} [monoid α] [mul_one_class β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] :
α × β →* β

Scalar multiplication as a monoid homomorphism.

Equations
@[simp]
theorem smul_monoid_hom_apply {α : Type u_5} {β : Type u_6} [monoid α] [mul_one_class β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] (ᾰ : α × β) :