Theorems · Definition · group theory

MulActionHom.casesOn

{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] →
              {motive : (X →ₑ[φ] Y) → Sort u} →
                (t : X →ₑ[φ] Y) →
                  ((toFun : X → Y) →
                      (map_smul' : ∀ (m : M) (x : X), toFun (m • x) = φ m • toFun x) →
                        motive { toFun := toFun, map_smul' := map_smul' }) →
                    motive t

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

1 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

SMulSMul