∀ {E : Type u_2} {F : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {R : Type u_3}
  {S : Type u_4} [inst_2 : Semiring R] [inst_3 : Ring S] [inst_4 : Module S E] [inst_5 : Module R F] {σ₁₂ : R →+* S}
  (f : F →ₛₗᵢ[σ₁₂] E), Function.Injective ⇑f