∀ {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₁]
  [inst_2 : DivisionSemiring R] [inst_3 : Module R M] [inst_4 : Module R M₁] {f : M →ₗ[R] R},
  f ≠ 0 → ∀ (x : M₁), (f.smulRight x).range = R ∙ x