(p : ENNReal) →
  {K : Type u_1} →
    {K' : Type u_2} →
      {V : Type u_4} →
        {V' : Type u_5} →
          [inst : Semiring K] →
            [inst_1 : Semiring K'] →
              {σ : K →+* K'} →
                [inst_2 : AddCommGroup V] →
                  [inst_3 : Module K V] →
                    [inst_4 : AddCommGroup V'] → [inst_5 : Module K' V'] → (V →ₛₗ[σ] V') → WithLp p V →ₛₗ[σ] WithLp p V'