Divisibility of linear functionals

If a non-zero-divisor a divides every value of a linear functional f : M →ₗ[R] R, then f is a times a linear functional (LinearMap.exists_smul_eq_of_forall_dvd). The quotients f x / a are unique because a is cancellable, and their uniqueness makes them linear.

theorem LinearMap.exists_smul_eq_of_forall_dvd {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {a : R} {f : M →ₗ[R] R} (ha : a ∈ nonZeroDivisors R) (h : ∀ (x : M), a ∣ f x) : ∃ (g : M →ₗ[R] R), a • g = f

If a is a non-zero-divisor dividing every value of a linear functional f, then f is a times a linear functional.