∀ {M₀ : Type u_1} [inst : TopologicalSpace M₀] [inst_1 : MulZeroOneClass M₀] [inst_2 : ContinuousMul M₀] (a b : M₀),
  SeparationQuotient.mk (a * b) = SeparationQuotient.mk a * SeparationQuotient.mk b