# Documentation

Mathlib.GroupTheory.GroupAction.Prod

# Prod instances for additive and multiplicative actions #

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

## Main declarations #

• smulMulHom /smulMonoidHom : Scalar multiplication bundled as a multiplicative/monoid homomorphism.

• Mathlib.GroupTheory.GroupAction.Option
• Mathlib.GroupTheory.GroupAction.Pi
• Mathlib.GroupTheory.GroupAction.Sigma
• Mathlib.GroupTheory.GroupAction.Sum

# Porting notes #

The to_additive attribute can be used to generate both the smul and vadd lemmas from the corresponding pow lemmas, as explained on zulip here: https://leanprover.zulipchat.com/#narrow/near/316087838

This was not done as part of the port in order to stay as close as possible to the mathlib3 code.

instance Prod.vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] :
VAdd M (α × β)
Equations
• Prod.vadd = { vadd := fun a p => (a +ᵥ p.fst, a +ᵥ p.snd) }
instance Prod.smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] :
SMul M (α × β)
Equations
• Prod.smul = { smul := fun a p => (a p.fst, a p.snd) }
@[simp]
theorem Prod.vadd_fst {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α × β) :
(a +ᵥ x).fst = a +ᵥ x.fst
@[simp]
theorem Prod.smul_fst {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α × β) :
(a x).fst = a x.fst
@[simp]
theorem Prod.vadd_snd {M : Type u_3} {α : Type u_2} {β : Type u_1} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α × β) :
(a +ᵥ x).snd = a +ᵥ x.snd
@[simp]
theorem Prod.smul_snd {M : Type u_3} {α : Type u_2} {β : Type u_1} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α × β) :
(a x).snd = a x.snd
@[simp]
theorem Prod.vadd_mk {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (b : α) (c : β) :
a +ᵥ (b, c) = (a +ᵥ b, a +ᵥ c)
@[simp]
theorem Prod.smul_mk {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (b : α) (c : β) :
a (b, c) = (a b, a c)
theorem Prod.vadd_def {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α × β) :
a +ᵥ x = (a +ᵥ x.fst, a +ᵥ x.snd)
theorem Prod.smul_def {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α × β) :
a x = (a x.fst, a x.snd)
@[simp]
theorem Prod.vadd_swap {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α × β) :
Prod.swap (a +ᵥ x) = a +ᵥ
@[simp]
theorem Prod.smul_swap {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α × β) :
Prod.swap (a x) = a
theorem Prod.smul_zero_mk {M : Type u_2} {β : Type u_3} [inst : SMul M β] {α : Type u_1} [inst : ] [inst : ] [inst : ] (a : M) (c : β) :
a (0, c) = (0, a c)
theorem Prod.smul_mk_zero {M : Type u_2} {α : Type u_3} [inst : SMul M α] {β : Type u_1} [inst : ] [inst : ] [inst : ] (a : M) (b : α) :
a (b, 0) = (a b, 0)
instance Prod.pow {E : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Pow α E] [inst : Pow β E] :
Pow (α × β) E
Equations
• Prod.pow = { pow := fun p c => (p.fst ^ c, p.snd ^ c) }
@[simp]
theorem Prod.pow_fst {E : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Pow α E] [inst : Pow β E] (p : α × β) (c : E) :
(p ^ c).fst = p.fst ^ c
@[simp]
theorem Prod.pow_snd {E : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Pow α E] [inst : Pow β E] (p : α × β) (c : E) :
(p ^ c).snd = p.snd ^ c
@[simp]
theorem Prod.pow_mk {E : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Pow α E] [inst : Pow β E] (c : E) (a : α) (b : β) :
(a, b) ^ c = (a ^ c, b ^ c)
theorem Prod.pow_def {E : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Pow α E] [inst : Pow β E] (p : α × β) (c : E) :
p ^ c = (p.fst ^ c, p.snd ^ c)
@[simp]
theorem Prod.pow_swap {E : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Pow α E] [inst : Pow β E] (p : α × β) (c : E) :
Prod.swap (p ^ c) = ^ c
instance Prod.vaddAssocClass {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : VAdd M N] [inst : ] [inst : ] :
VAddAssocClass M N (α × β)
Equations
def Prod.vaddAssocClass.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : VAdd M N] [inst : ] [inst : ] :
VAddAssocClass M N (α × β)
Equations
instance Prod.isScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst : SMul M β] [inst : SMul N α] [inst : SMul N β] [inst : SMul M N] [inst : ] [inst : ] :
IsScalarTower M N (α × β)
Equations
instance Prod.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : ] [inst : ] :
VAddCommClass M N (α × β)
Equations
def Prod.vaddCommClass.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : ] [inst : ] :
VAddCommClass M N (α × β)
Equations
instance Prod.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst : SMul M β] [inst : SMul N α] [inst : SMul N β] [inst : ] [inst : ] :
SMulCommClass M N (α × β)
Equations
def Prod.isCentralVAdd.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd Mᵃᵒᵖ α] [inst : VAdd Mᵃᵒᵖ β] [inst : ] [inst : ] :
IsCentralVAdd M (α × β)
Equations
instance Prod.isCentralVAdd {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd Mᵃᵒᵖ α] [inst : VAdd Mᵃᵒᵖ β] [inst : ] [inst : ] :
IsCentralVAdd M (α × β)
Equations
instance Prod.isCentralScalar {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : SMul Mᵐᵒᵖ α] [inst : SMul Mᵐᵒᵖ β] [inst : ] [inst : ] :
Equations
instance Prod.faithfulVAddLeft {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : ] [inst : ] :
FaithfulVAdd M (α × β)
Equations
def Prod.faithfulVAddLeft.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : ] [inst : ] :
FaithfulVAdd M (α × β)
Equations
abbrev Prod.faithfulVAddLeft.match_1 {β : Type u_1} (motive : Prop) :
(x : ) → ((b : β) → motive (_ : )) → motive x
Equations
instance Prod.faithfulSMulLeft {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : ] [inst : ] :
FaithfulSMul M (α × β)
Equations
def Prod.faithfulVAddRight.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : ] [inst : ] :
FaithfulVAdd M (α × β)
Equations
instance Prod.faithfulVAddRight {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : ] [inst : ] :
FaithfulVAdd M (α × β)
Equations
instance Prod.faithfulSMulRight {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : ] [inst : ] :
FaithfulSMul M (α × β)
Equations
def Prod.vaddCommClassBoth.proof_1 {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add N] [inst : Add P] [inst : VAdd M N] [inst : VAdd M P] [inst : ] [inst : ] :
VAddCommClass M (N × P) (N × P)
Equations
instance Prod.vaddCommClassBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add N] [inst : Add P] [inst : VAdd M N] [inst : VAdd M P] [inst : ] [inst : ] :
VAddCommClass M (N × P) (N × P)
Equations
instance Prod.smulCommClassBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul N] [inst : Mul P] [inst : SMul M N] [inst : SMul M P] [inst : ] [inst : ] :
SMulCommClass M (N × P) (N × P)
Equations
instance Prod.isScalarTowerBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul N] [inst : Mul P] [inst : SMul M N] [inst : SMul M P] [inst : ] [inst : ] :
IsScalarTower M (N × P) (N × P)
Equations
instance Prod.addAction {M : Type u_1} {α : Type u_2} {β : Type u_3} :
{x : } → [inst : ] → [inst : ] → AddAction M (α × β)
Equations
• One or more equations did not get rendered due to their size.
def Prod.addAction.proof_2 {M : Type u_3} {α : Type u_1} {β : Type u_2} :
∀ {x : } [inst : ] [inst_1 : ] (x_1 x_2 : M) (x_3 : α × β), ((x_1 + x_2 +ᵥ x_3).fst, (x_1 + x_2 +ᵥ x_3).snd) = ((x_1 +ᵥ (x_2 +ᵥ x_3)).fst, (x_1 +ᵥ (x_2 +ᵥ x_3)).snd)
Equations
abbrev Prod.addAction.match_1 {α : Type u_1} {β : Type u_2} (motive : α × βProp) :
(x : α × β) → ((fst : α) → (snd : β) → motive (fst, snd)) → motive x
Equations
def Prod.addAction.proof_1 {M : Type u_3} {α : Type u_1} {β : Type u_2} :
∀ {x : } [inst : ] [inst_1 : ] (x_1 : α × β), 0 +ᵥ x_1 = x_1
Equations
instance Prod.mulAction {M : Type u_1} {α : Type u_2} {β : Type u_3} :
{x : } → [inst : ] → [inst : ] → MulAction M (α × β)
Equations
• One or more equations did not get rendered due to their size.
instance Prod.smulZeroClass {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Zero M] [inst : Zero N] [inst : ] [inst : ] :
Equations
instance Prod.distribSMul {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : ] [inst : ] [inst : ] [inst : ] :
DistribSMul R (M × N)
Equations
instance Prod.distribMulAction {R : Type u_1} {M : Type u_2} {N : Type u_3} :
{x : } → [inst : ] → [inst_1 : ] → [inst_2 : ] → [inst_3 : ] → DistribMulAction R (M × N)
Equations
• Prod.distribMulAction = let src := Prod.mulAction; let src_1 := Prod.distribSMul; DistribMulAction.mk (_ : ∀ (a : R), a 0 = 0) (_ : ∀ (a : R) (x y : M × N), a (x + y) = a x + a y)
instance Prod.mulDistribMulAction {R : Type u_1} {M : Type u_2} {N : Type u_3} :
{x : } → [inst : ] → [inst_1 : ] → [inst_2 : ] → [inst_3 : ] → MulDistribMulAction R (M × N)
Equations
• One or more equations did not get rendered due to their size.

### Scalar multiplication as a homomorphism #

@[simp]
theorem smulMulHom_apply {α : Type u_1} {β : Type u_2} [inst : ] [inst : Mul β] [inst : ] [inst : ] [inst : ] (a : α × β) :
smulMulHom a = a.fst a.snd
def smulMulHom {α : Type u_1} {β : Type u_2} [inst : ] [inst : Mul β] [inst : ] [inst : ] [inst : ] :
α × β →ₙ* β

Scalar multiplication as a multiplicative homomorphism.

Equations
• smulMulHom = { toFun := fun a => a.fst a.snd, map_mul' := (_ : ∀ (x x_1 : α × β), (x.fst * x_1.fst) (x.snd * x_1.snd) = x.fst x.snd * x_1.fst x_1.snd) }
@[simp]
theorem smulMonoidHom_apply {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] :
∀ (a : α × β), smulMonoidHom a = MulHom.toFun smulMulHom a
def smulMonoidHom {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] :
α × β →* β

Scalar multiplication as a monoid homomorphism.

Equations
• One or more equations did not get rendered due to their size.