Finitely many proportionality classes force dimension at most one

theorem MagnitudeConjecture.FiniteKernel.finrank_le_one_of_finite_proportional_classes {k : Type u} [Field k] [Infinite k] {V : Type v} [AddCommGroup V] [Module k V] {ι : Type w} [Finite ι] (label : { v : V // v ≠ 0 } → ι) (hlabel : ∀ (v w : { v : V // v ≠ 0 }), label v = label w → ∃ (c : k), c • ↑v = ↑w) : Module.finrank k V ≤ 1

Over an infinite field, a finite labelling of nonzero vectors whose equal labels imply proportionality forces dimension at most one.