Theorems · Definition · group theory

MulActionSemiHomClass.toMulActionHom

{M : Type u_2} →
  {N : Type u_3} →
    {φ : M → N} →
      {X : Type u_5} →
        [inst : SMul M X] →
          {Y : Type u_6} →
            [inst_1 : SMul N Y] →
              {F : Type u_8} → [inst_2 : FunLike F X Y] → [MulActionSemiHomClass F φ X Y] → F → X →ₑ[φ] Y

Turn an element of a type F satisfying MulActionSemiHomClass F φ X Y into an actual MulActionHom. This is declared as the default coercion from F to MulActionSemiHom φ X Y.

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

5 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

SMulSMulFunLikeMulActionSemiHomClass