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/Algebra/Group/Action/Option.lean
Mathlib/Algebra/Group/Action/Pi.lean
Mathlib/Algebra/Group/Action/Sigma.lean
Mathlib/Algebra/Group/Action/Sum.lean
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.
Scalar multiplication as a homomorphism #
Scalar multiplication as a multiplicative homomorphism.
Equations
Instances For
Scalar multiplication as a monoid homomorphism.
Equations
Instances For
Construct a MulAction
by a product monoid from MulAction
s by the factors.
This is not an instance to avoid diamonds for example when α := M × N
.
Equations
Instances For
Construct an AddAction
by a product monoid from AddAction
s by the factors.
This is not an instance to avoid diamonds for example when α := M × N
.