∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra S R] (r : R → R → Prop)
  (x y : S),
  { toQuot := Quot.mk (RingQuot.Rel r) ((algebraMap S R) (x * y)) } =
    { toQuot := Quot.mk (RingQuot.Rel r) ((algebraMap S R) x) } *
      { toQuot := Quot.mk (RingQuot.Rel r) ((algebraMap S R) y) }