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.
See also #
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.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 : VAddAssocClass M N α]
[inst : VAddAssocClass M N β]
:
VAddAssocClass M N (α × β)
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 : VAddAssocClass M N α]
[inst : VAddAssocClass M N β]
:
VAddAssocClass M N (α × β)
Equations
- (_ : VAddAssocClass M N (α × β)) = (_ : VAddAssocClass M N (α × β))
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 : IsScalarTower M N α]
[inst : IsScalarTower M N β]
:
IsScalarTower M N (α × β)
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 : VAddCommClass M N α]
[inst : VAddCommClass M N β]
:
VAddCommClass M N (α × β)
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 : VAddCommClass M N α]
[inst : VAddCommClass M N β]
:
VAddCommClass M N (α × β)
Equations
- (_ : VAddCommClass M N (α × β)) = (_ : VAddCommClass M N (α × β))
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 : SMulCommClass M N α]
[inst : SMulCommClass M N β]
:
SMulCommClass M N (α × β)
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 : IsCentralVAdd M α]
[inst : IsCentralVAdd M β]
:
IsCentralVAdd M (α × β)
Equations
- (_ : IsCentralVAdd M (α × β)) = (_ : IsCentralVAdd M (α × β))
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 : IsCentralVAdd M α]
[inst : IsCentralVAdd M β]
:
IsCentralVAdd M (α × β)
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 : IsCentralScalar M α]
[inst : IsCentralScalar M β]
:
IsCentralScalar M (α × β)
instance
Prod.faithfulVAddLeft
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : VAdd M α]
[inst : VAdd M β]
[inst : FaithfulVAdd M α]
[inst : Nonempty β]
:
FaithfulVAdd M (α × β)
def
Prod.faithfulVAddLeft.proof_1
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : VAdd M α]
[inst : VAdd M β]
[inst : FaithfulVAdd M α]
[inst : Nonempty β]
:
FaithfulVAdd M (α × β)
Equations
- (_ : FaithfulVAdd M (α × β)) = (_ : FaithfulVAdd M (α × β))
Equations
- Prod.faithfulVAddLeft.match_1 motive x h_1 = Nonempty.casesOn x fun val => h_1 val
instance
Prod.faithfulSMulLeft
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : SMul M α]
[inst : SMul M β]
[inst : FaithfulSMul M α]
[inst : Nonempty β]
:
FaithfulSMul M (α × β)
def
Prod.faithfulVAddRight.proof_1
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : VAdd M α]
[inst : VAdd M β]
[inst : Nonempty α]
[inst : FaithfulVAdd M β]
:
FaithfulVAdd M (α × β)
Equations
- (_ : FaithfulVAdd M (α × β)) = (_ : FaithfulVAdd M (α × β))
instance
Prod.faithfulVAddRight
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : VAdd M α]
[inst : VAdd M β]
[inst : Nonempty α]
[inst : FaithfulVAdd M β]
:
FaithfulVAdd M (α × β)
instance
Prod.faithfulSMulRight
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : SMul M α]
[inst : SMul M β]
[inst : Nonempty α]
[inst : FaithfulSMul M β]
:
FaithfulSMul M (α × β)
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 : VAddCommClass M N N]
[inst : VAddCommClass M P P]
:
VAddCommClass M (N × P) (N × P)
Equations
- (_ : VAddCommClass M (N × P) (N × P)) = (_ : VAddCommClass M (N × P) (N × P))
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 : VAddCommClass M N N]
[inst : VAddCommClass M P P]
:
VAddCommClass M (N × P) (N × P)
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 : SMulCommClass M N N]
[inst : SMulCommClass M P P]
:
SMulCommClass M (N × P) (N × P)
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 : IsScalarTower M N N]
[inst : IsScalarTower M P P]
:
IsScalarTower M (N × P) (N × P)
abbrev
Prod.addAction.match_1
{α : Type u_1}
{β : Type u_2}
(motive : α × β → Prop)
:
(x : α × β) → ((fst : α) → (snd : β) → motive (fst, snd)) → motive x
Equations
- Prod.addAction.match_1 motive x h_1 = Prod.casesOn x fun fst snd => h_1 fst snd
instance
Prod.smulZeroClass
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : Zero N]
[inst : SMulZeroClass R M]
[inst : SMulZeroClass R N]
:
SMulZeroClass R (M × N)
Equations
- Prod.smulZeroClass = SMulZeroClass.mk (_ : ∀ (x : R), ((x • 0).fst, (x • 0).snd) = (0.fst, 0.snd))
instance
Prod.distribSMul
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : AddZeroClass M]
[inst : AddZeroClass N]
[inst : DistribSMul R M]
[inst : DistribSMul R N]
:
DistribSMul R (M × N)
instance
Prod.distribMulAction
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
:
{x : Monoid R} →
[inst : AddMonoid M] →
[inst_1 : AddMonoid N] →
[inst_2 : DistribMulAction R M] → [inst_3 : DistribMulAction R N] → DistribMulAction R (M × N)
instance
Prod.mulDistribMulAction
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
:
{x : Monoid R} →
[inst : Monoid M] →
[inst_1 : Monoid N] →
[inst_2 : MulDistribMulAction R M] → [inst_3 : MulDistribMulAction R N] → 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 : Monoid α]
[inst : Mul β]
[inst : MulAction α β]
[inst : IsScalarTower α β β]
[inst : SMulCommClass α β β]
(a : α × β)
:
def
smulMulHom
{α : Type u_1}
{β : Type u_2}
[inst : Monoid α]
[inst : Mul β]
[inst : MulAction α β]
[inst : IsScalarTower α β β]
[inst : SMulCommClass α β β]
:
Scalar multiplication as a multiplicative homomorphism.
@[simp]
theorem
smulMonoidHom_apply
{α : Type u_1}
{β : Type u_2}
[inst : Monoid α]
[inst : MulOneClass β]
[inst : MulAction α β]
[inst : IsScalarTower α β β]
[inst : SMulCommClass α β β]
:
∀ (a : α × β), ↑smulMonoidHom a = MulHom.toFun smulMulHom a
def
smulMonoidHom
{α : Type u_1}
{β : Type u_2}
[inst : Monoid α]
[inst : MulOneClass β]
[inst : MulAction α β]
[inst : IsScalarTower α β β]
[inst : SMulCommClass α β β]
:
Scalar multiplication as a monoid homomorphism.
Equations
- One or more equations did not get rendered due to their size.