Actions of groups with zero

The scalar rescaling identity TauCeti.div_mul_smul_smul_cancel_left cancels a nonzero factor in the denominator against a scalar action, including when the remaining denominator is zero.

theorem TauCeti.div_mul_smul_smul_cancel_left {K : Type u_1} {M : Type u_2} [GroupWithZero K] [MulAction K M] {k : K} (hk : k ≠ 0) (a b : K) (v : M) : (a / (k * b)) • k • v = (a / b) • v

Rescaling k • v by a / (k * b) is rescaling v by a / b.