∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (x : E) (y : F) (H : ∀ (c : R), c • x = 0 → c • y = 0),
  (LinearPMap.mkSpanSingleton' x y H).domain = R ∙ x