apply (QuadRing.ext_iff _ _).2
F : Type u_1
a b : F
inst✝ : CommRing F
r s : F
⊢ { b1 := r * s, b2 := 0 } = { b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }
F : Type u_1
a b : F
inst✝ : CommRing F
r s : F
⊢ { b1 := r * s, b2 := 0 }.b1 = ({ b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }).b1 ∧
    { b1 := r * s, b2 := 0 }.b2 = ({ b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }).b2