∀ {F : Type u_2} (R : Type u_1) (S : Type u_3) [inst : FunLike F R S] [inst_1 : DivisionRing R]
  [inst_2 : NormedDivisionRing S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective ⇑f) (a : R),
  SubNegMonoid.zsmul 0 a = 0