# 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_5} {β : Type u_6} [VAdd M α] [VAdd M β] :
VAdd M (α × β)
Equations
• Prod.vadd = { vadd := fun (a : M) (p : α × β) => (a +ᵥ p.1, a +ᵥ p.2) }
instance Prod.smul {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] :
SMul M (α × β)
Equations
• Prod.smul = { smul := fun (a : M) (p : α × β) => (a p.1, a p.2) }
@[simp]
theorem Prod.vadd_fst {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] (a : M) (x : α × β) :
(a +ᵥ x).1 = a +ᵥ x.1
@[simp]
theorem Prod.smul_fst {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] (a : M) (x : α × β) :
(a x).1 = a x.1
@[simp]
theorem Prod.vadd_snd {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] (a : M) (x : α × β) :
(a +ᵥ x).2 = a +ᵥ x.2
@[simp]
theorem Prod.smul_snd {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] (a : M) (x : α × β) :
(a x).2 = a x.2
@[simp]
theorem Prod.vadd_mk {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] (a : M) (b : α) (c : β) :
a +ᵥ (b, c) = (a +ᵥ b, a +ᵥ c)
@[simp]
theorem Prod.smul_mk {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul 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} [VAdd M α] [VAdd M β] (a : M) (x : α × β) :
a +ᵥ x = (a +ᵥ x.1, a +ᵥ x.2)
theorem Prod.smul_def {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] (a : M) (x : α × β) :
a x = (a x.1, a x.2)
@[simp]
theorem Prod.vadd_swap {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [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} [SMul M α] [SMul M β] (a : M) (x : α × β) :
(a x).swap = a x.swap
theorem Prod.smul_zero_mk {M : Type u_1} {β : Type u_6} [SMul M β] {α : Type u_7} [] [] [] (a : M) (c : β) :
a (0, c) = (0, a c)
theorem Prod.smul_mk_zero {M : Type u_1} {α : Type u_5} [SMul M α] {β : Type u_7} [] [] [] (a : M) (b : α) :
a (b, 0) = (a b, 0)
instance Prod.pow {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [Pow β E] :
Pow (α × β) E
Equations
• Prod.pow = { pow := fun (p : α × β) (c : E) => (p.1 ^ c, p.2 ^ c) }
@[simp]
theorem Prod.pow_fst {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [Pow β E] (p : α × β) (c : E) :
(p ^ c).1 = p.1 ^ c
@[simp]
theorem Prod.pow_snd {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [Pow β E] (p : α × β) (c : E) :
(p ^ c).2 = p.2 ^ c
@[simp]
theorem Prod.pow_mk {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [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} [Pow α E] [Pow β E] (p : α × β) (c : E) :
p ^ c = (p.1 ^ c, p.2 ^ c)
@[simp]
theorem Prod.pow_swap {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [Pow β E] (p : α × β) (c : E) :
(p ^ c).swap = p.swap ^ c
instance Prod.vaddAssocClass {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [VAdd N α] [VAdd N β] [VAdd M N] [] [] :
VAddAssocClass M N (α × β)
Equations
• =
instance Prod.isScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [SMul M N] [] [] :
IsScalarTower M N (α × β)
Equations
• =
instance Prod.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [VAdd N α] [VAdd N β] [] [] :
VAddCommClass M N (α × β)
Equations
• =
instance Prod.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [] [] :
SMulCommClass M N (α × β)
Equations
• =
instance Prod.isCentralVAdd {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [VAdd Mᵃᵒᵖ α] [VAdd Mᵃᵒᵖ β] [] [] :
IsCentralVAdd M (α × β)
Equations
• =
instance Prod.isCentralScalar {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [SMul Mᵐᵒᵖ α] [SMul Mᵐᵒᵖ β] [] [] :
Equations
• =
abbrev Prod.faithfulVAddLeft.match_1 {β : Type u_1} (motive : Prop) :
∀ (x : ), (∀ (b : β), motive )motive x
Equations
• =
Instances For
instance Prod.faithfulVAddLeft {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [] [] :
FaithfulVAdd M (α × β)
Equations
• =
instance Prod.faithfulSMulLeft {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [] [] :
FaithfulSMul M (α × β)
Equations
• =
instance Prod.faithfulVAddRight {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [] [] :
FaithfulVAdd M (α × β)
Equations
• =
instance Prod.faithfulSMulRight {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [] [] :
FaithfulSMul M (α × β)
Equations
• =
instance Prod.vaddCommClassBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add N] [Add P] [VAdd M N] [VAdd M P] [] [] :
VAddCommClass M (N × P) (N × P)
Equations
• =
instance Prod.smulCommClassBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul N] [Mul P] [SMul M N] [SMul M P] [] [] :
SMulCommClass M (N × P) (N × P)
Equations
• =
instance Prod.isScalarTowerBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul N] [Mul P] [SMul M N] [SMul M P] [] [] :
IsScalarTower M (N × P) (N × P)
Equations
• =
instance Prod.addAction {M : Type u_1} {α : Type u_5} {β : Type u_6} [] [] [] :
AddAction M (α × β)
Equations
theorem Prod.addAction.proof_1 {M : Type u_3} {α : Type u_1} {β : Type u_2} [] [] [] :
∀ (x : α × β), 0 +ᵥ x = x
abbrev Prod.addAction.match_1 {α : Type u_1} {β : Type u_2} (motive : α × βProp) :
∀ (x : α × β), (∀ (fst : α) (snd : β), motive (fst, snd))motive x
Equations
• =
Instances For
theorem Prod.addAction.proof_2 {M : Type u_3} {α : Type u_1} {β : Type u_2} [] [] [] :
∀ (x x_1 : M) (x_2 : α × β), (x + x_1 +ᵥ x_2.1, x + x_1 +ᵥ x_2.2) = (x +ᵥ (x_1 +ᵥ x_2).1, x +ᵥ (x_1 +ᵥ x_2).2)
instance Prod.mulAction {M : Type u_1} {α : Type u_5} {β : Type u_6} [] [] [] :
MulAction M (α × β)
Equations
• Prod.mulAction =
instance Prod.smulZeroClass {R : Type u_7} {M : Type u_8} {N : Type u_9} [Zero M] [Zero N] [] [] :
Equations
• Prod.smulZeroClass =
instance Prod.distribSMul {R : Type u_7} {M : Type u_8} {N : Type u_9} [] [] [] [] :
DistribSMul R (M × N)
Equations
• Prod.distribSMul =
instance Prod.distribMulAction {M : Type u_1} {N : Type u_2} {R : Type u_7} [] [] [] [] [] :
Equations
• Prod.distribMulAction = let __src := Prod.mulAction; let __src_1 := Prod.distribSMul;
instance Prod.mulDistribMulAction {M : Type u_1} {N : Type u_2} {R : Type u_7} [] [] [] [] [] :
Equations
• Prod.mulDistribMulAction =

### Scalar multiplication as a homomorphism #

@[simp]
theorem smulMulHom_apply {α : Type u_5} {β : Type u_6} [] [Mul β] [] [] [] (a : α × β) :
smulMulHom a = a.1 a.2
def smulMulHom {α : Type u_5} {β : Type u_6} [] [Mul β] [] [] [] :
α × β →ₙ* β

Scalar multiplication as a multiplicative homomorphism.

Equations
• smulMulHom = { toFun := fun (a : α × β) => a.1 a.2, map_mul' := }
Instances For
@[simp]
theorem smulMonoidHom_apply {α : Type u_5} {β : Type u_6} [] [] [] [] [] :
∀ (a : α × β), smulMonoidHom a = smulMulHom.toFun a
def smulMonoidHom {α : Type u_5} {β : Type u_6} [] [] [] [] [] :
α × β →* β

Scalar multiplication as a monoid homomorphism.

Equations
• smulMonoidHom = let __src := smulMulHom; { toFun := __src.toFun, map_one' := , map_mul' := }
Instances For
abbrev AddAction.prodOfVAddCommClass (M : Type u_1) (N : Type u_2) (α : Type u_5) [] [] [] [] [] :
AddAction (M × N) α

Construct an AddAction by a product monoid from AddActions by the factors. This is not an instance to avoid diamonds for example when α := M × N.

Equations
Instances For
theorem AddAction.prodOfVAddCommClass.proof_1 (M : Type u_2) (N : Type u_3) (α : Type u_1) [] [] [] [] (a : α) :
0 +ᵥ (0.2 +ᵥ a) = a
theorem AddAction.prodOfVAddCommClass.proof_2 (M : Type u_1) (N : Type u_2) (α : Type u_3) [] [] [] [] [] (x : M × N) (y : M × N) (a : α) :
x.1 + y.1 +ᵥ (x.2 + y.2 +ᵥ a) = x.1 +ᵥ (x.2 +ᵥ (y.1 +ᵥ (y.2 +ᵥ a)))
@[reducible, inline]
abbrev MulAction.prodOfSMulCommClass (M : Type u_1) (N : Type u_2) (α : Type u_5) [] [] [] [] [] :
MulAction (M × N) α

Construct a MulAction by a product monoid from MulActions by the factors. This is not an instance to avoid diamonds for example when α := M × N.

Equations
Instances For
theorem AddAction.prodEquiv.proof_2 (M : Type u_3) (N : Type u_2) (α : Type u_1) [] [] (_insts : (x : ) ×' (x_1 : ) ×' ) :
theorem AddAction.prodEquiv.proof_3 (M : Type u_3) (N : Type u_2) (α : Type u_1) [] [] :
∀ (x : AddAction (M × N) α), (fun (_insts : (x : ) ×' (x_1 : ) ×' ) => let_fun this := ; ) ((fun (x : AddAction (M × N) α) => , , ) x) = x
theorem AddAction.prodEquiv.proof_4 (M : Type u_1) (N : Type u_3) (α : Type u_2) [] [] :
∀ (x : (x : ) ×' (x_1 : ) ×' ), (fun (x : AddAction (M × N) α) => , , ) ((fun (_insts : (x : ) ×' (x_1 : ) ×' ) => let_fun this := ; ) x) = x
def AddAction.prodEquiv (M : Type u_1) (N : Type u_2) (α : Type u_5) [] [] :
AddAction (M × N) α (x : ) ×' (x_1 : ) ×'

An AddAction by a product monoid is equivalent to commuting AddActions by the factors.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddAction.prodEquiv.proof_1 (M : Type u_3) (N : Type u_2) (α : Type u_1) [] [] :
∀ (x : AddAction (M × N) α),
def MulAction.prodEquiv (M : Type u_1) (N : Type u_2) (α : Type u_5) [] [] :
MulAction (M × N) α (x : ) ×' (x_1 : ) ×'

A MulAction by a product monoid is equivalent to commuting MulActions by the factors.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev DistribMulAction.prodOfSMulCommClass (M : Type u_1) (N : Type u_2) (α : Type u_5) [] [] [] [] [] [] :

Construct a DistribMulAction by a product monoid from DistribMulActions by the factors.

Equations
• = let __spread.0 := ;
Instances For
def DistribMulAction.prodEquiv (M : Type u_1) (N : Type u_2) (α : Type u_5) [] [] [] :
DistribMulAction (M × N) α (x : ) ×' (x_1 : ) ×'

A DistribMulAction by a product monoid is equivalent to commuting DistribMulActions by the factors.

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