∀ (𝕜 : Type u_1) (A : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A],
  Function.Injective ⇑(Unitization.splitMul 𝕜 A)