Theorems · Inductive type · group theory

MulDistribMulActionHom

{M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        (M →* N) →
          (A : Type u_4) →
            [inst_2 : Monoid A] →
              [MulDistribMulAction M A] →
                (B : Type u_5) → [inst : Monoid B] → [MulDistribMulAction N B] → Type (max u_4 u_5)

Equivariant monoid homomorphisms.

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

25 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

MonoidMonoidMonoidMulDistribMulActionMonoidMulDistribMulAction