{R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      {inst : Semiring R} →
        {inst_1 : AddCommMonoid E₁} →
          {inst_2 : PartialOrder E₁} →
            {inst_3 : AddCommMonoid E₂} →
              {inst_4 : PartialOrder E₂} → {inst_5 : Module R E₁} → {inst_6 : Module R E₂} → (E₁ →ₚ[R] E₂) → ℕ