Theorems · Definition · group theory

SMulCommClass.toDistribMulActionHom

{M : Type u_13} →
  (N : Type u_11) →
    (A : Type u_12) →
      [inst : Monoid N] →
        [inst_1 : AddMonoid A] →
          [inst_2 : DistribSMul M A] → [inst_3 : DistribMulAction N A] → [SMulCommClass M N A] → M → A →+[N] A

If DistribMulAction of M and N on A commute, then for each c : M, (c • ·) is an N-action additive homomorphism.

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

MonoidAddMonoidDistribSMulDistribMulActionSMulCommClass