mathlib3documentation

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 #

• smul_mul_hom/smul_monoid_hom: Scalar multiplication bundled as a multiplicative/monoid homomorphism.

• group_theory.group_action.option
• group_theory.group_action.pi
• group_theory.group_action.sigma
• group_theory.group_action.sum
@[protected, instance]
def prod.has_vadd {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] :
× β)
Equations
@[protected, instance]
def prod.has_smul {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] :
× β)
Equations
@[simp]
theorem prod.vadd_fst {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] (a : M) (x : α × β) :
(a +ᵥ x).fst = a +ᵥ x.fst
@[simp]
theorem prod.smul_fst {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] (a : M) (x : α × β) :
(a x).fst = a x.fst
@[simp]
theorem prod.smul_snd {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] (a : M) (x : α × β) :
(a x).snd = a x.snd
@[simp]
theorem prod.vadd_snd {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] (a : M) (x : α × β) :
(a +ᵥ x).snd = a +ᵥ x.snd
@[simp]
theorem prod.smul_mk {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] (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} [ α] [ β] (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} [ α] [ β] (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} [ α] [ β] (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} [ α] [ β] (a : M) (x : α × β) :
(a +ᵥ x).swap = a +ᵥ x.swap
@[simp]
theorem prod.smul_swap {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] (a : M) (x : α × β) :
(a x).swap = a x.swap
theorem prod.smul_zero_mk {M : Type u_1} {β : Type u_6} [ β] {α : Type u_2} [monoid M] [add_monoid α] [ α] (a : M) (c : β) :
a (0, c) = (0, a c)
theorem prod.smul_mk_zero {M : Type u_1} {α : Type u_5} [ α] {β : Type u_2} [monoid M] [add_monoid β] [ β] (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} [ E] [ E] :
has_pow × β) E
Equations
@[simp]
theorem prod.pow_fst {E : Type u_4} {α : Type u_5} {β : Type u_6} [ E] [ 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} [ E] [ 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} [ E] [ 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} [ E] [ 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} [ E] [ 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} [ α] [ β] [ α] [ β] [ N] [ α] [ β] :
× β)
@[protected, instance]
def prod.is_scalar_tower {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [ α] [ β] [ α] [ β] [ N] [ α] [ β] :
× β)
@[protected, instance]
def prod.vadd_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [ α] [ β] [ α] [ β] [ α] [ β] :
× β)
@[protected, instance]
def prod.smul_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [ α] [ β] [ α] [ β] [ α] [ β] :
× β)
@[protected, instance]
def prod.is_central_vadd {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] [ α] [ β] [ α] [ β] :
× β)
@[protected, instance]
def prod.is_central_scalar {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] [ α] [ β] [ α] [ β] :
× β)
@[protected, instance]
def prod.has_faithful_vadd_left {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] [ α] [nonempty β] :
× β)
@[protected, instance]
def prod.has_faithful_smul_left {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] [ α] [nonempty β] :
× β)
@[protected, instance]
def prod.has_faithful_vadd_right {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] [nonempty α] [ β] :
× β)
@[protected, instance]
def prod.has_faithful_smul_right {M : Type u_1} {α : Type u_5} {β : Type u_6} [ α] [ β] [nonempty α] [ β] :
× β)
@[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] [ N] [ P] [ N] [ P] :
(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] [ N] [ P] [ N] [ P] :
(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] [ N] [ P] [ N] [ P] :
(N × P) (N × P)
@[protected, instance]
def prod.add_action {M : Type u_1} {α : Type u_5} {β : Type u_6} {m : add_monoid M} [ α] [ β] :
× β)
Equations
@[protected, instance]
def prod.mul_action {M : Type u_1} {α : Type u_5} {β : Type u_6} {m : monoid 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] [ M] [ N] :
(M × N)
Equations
@[protected, instance]
def prod.distrib_smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] :
(M × N)
Equations
@[protected, instance]
def prod.distrib_mul_action {R : Type u_1} {M : Type u_2} {N : Type u_3} {r : monoid R} [add_monoid M] [add_monoid N] [ M] [ N] :
(M × N)
Equations
@[protected, instance]
def prod.mul_distrib_mul_action {R : Type u_1} {M : Type u_2} {N : Type u_3} {r : monoid R} [monoid M] [monoid N]  :
(M × N)
Equations

Scalar multiplication as a homomorphism #

@[simp]
theorem smul_mul_hom_apply {α : Type u_5} {β : Type u_6} [monoid α] [has_mul β] [ β] [ β] [ β] (a : α × β) :
= a.fst a.snd
def smul_mul_hom {α : Type u_5} {β : Type u_6} [monoid α] [has_mul β] [ β] [ β] [ β] :
α × β →ₙ* β

Scalar multiplication as a multiplicative homomorphism.

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

Scalar multiplication as a monoid homomorphism.

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