theorem div_left_injective₀ {G₀ : Type u_1} [CommGroupWithZero G₀] {c : G₀} (hc : c ≠ 0) : Function.Injective fun (x : G₀) => x / c