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 #

See also #

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.

source
theorem Prod.smul_zero_mk {M : Type u_1} {β : Type u_6} [SMul M β] {α : Type u_7} [Monoid M] [AddMonoid α] [DistribMulAction M α] (a : M) (c : β) :
a • (0, c) = (0, a • c)
source
theorem Prod.smul_mk_zero {M : Type u_1} {α : Type u_5} [SMul M α] {β : Type u_7} [Monoid M] [AddMonoid β] [DistribMulAction M β] (a : M) (b : α) :
a • (b, 0) = (a • b, 0)
source
instance Prod.smulZeroClass {R : Type u_7} {M : Type u_8} {N : Type u_9} [Zero M] [Zero N] [SMulZeroClass R M] [SMulZeroClass R N] :
SMulZeroClass R (M × N)
Equations
source
instance Prod.distribSMul {R : Type u_7} {M : Type u_8} {N : Type u_9} [AddZeroClass M] [AddZeroClass N] [DistribSMul R M] [DistribSMul R N] :
DistribSMul R (M × N)
Equations
source
instance Prod.distribMulAction {M : Type u_1} {N : Type u_2} {R : Type u_7} [Monoid R] [AddMonoid M] [AddMonoid N] [DistribMulAction R M] [DistribMulAction R N] :
DistribMulAction R (M × N)
Equations
  • Prod.distribMulAction = let __src := Prod.mulAction; let __src_1 := Prod.distribSMul; DistribMulAction.mk ⋯ ⋯
source
instance Prod.mulDistribMulAction {M : Type u_1} {N : Type u_2} {R : Type u_7} [Monoid R] [Monoid M] [Monoid N] [MulDistribMulAction R M] [MulDistribMulAction R N] :
MulDistribMulAction R (M × N)
Equations

Scalar multiplication as a homomorphism #

source
@[reducible, inline]
abbrev DistribMulAction.prodOfSMulCommClass (M : Type u_1) (N : Type u_2) (α : Type u_5) [Monoid M] [Monoid N] [AddMonoid α] [DistribMulAction M α] [DistribMulAction N α] [SMulCommClass M N α] :
DistribMulAction (M × N) α

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

Equations
Instances For
    source
    def DistribMulAction.prodEquiv (M : Type u_1) (N : Type u_2) (α : Type u_5) [Monoid M] [Monoid N] [AddMonoid α] :
    DistribMulAction (M × N) α ≃ (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α

    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