Theorems · Inductive type · group theory

MulActionSemiHomClass

(F : Type u_8) →
  {M : outParam (Type u_9)} →
    {N : outParam (Type u_10)} →
      outParam (M → N) →
        (X : outParam (Type u_11)) → (Y : outParam (Type u_12)) → [SMul M X] → [SMul N Y] → [FunLike F X Y] → Prop

MulActionSemiHomClass F φ X Y states that F is a type of morphisms which are φ-equivariant. You should extend this class when you extend MulActionHom.

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

13 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

SMulSMulFunLike