theorem Rings.ring_product_iff_nontrivial_idempotent (Q : Type u) [CommRing Q] : (∃ (R : Type u) (S : Type u) (x : Ring R) (x_1 : Ring S) (_ : Nontrivial R) (_ : Nontrivial S), Nonempty (Q ≃+* R × S)) ↔ ∃ (e : Q), IsIdempotentElem e ∧ e ≠ 0 ∧ e ≠ 1