Simplicity is preserved by ring isomorphisms/surjective ring homomorphisms

If R is a simple (non-assoc) ring and there exists surjective f : R →+* S where S is nontrivial, then S is also simple. If R is a simple (non-unital non-assoc) ring then any ring isomorphic to R is also simple.

theorem IsSimpleRing.of_surjective {R : Type u_1} {S : Type u_2} [NonAssocRing R] [NonAssocRing S] [Nontrivial S] (f : R →+* S) (h : IsSimpleRing R) (hf : Function.Surjective ⇑f) : IsSimpleRing S

theorem IsSimpleRing.of_ringEquiv {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R ≃+* S) (h : IsSimpleRing R) : IsSimpleRing S

theorem isSimpleRing_iff_isTwoSided_imp {R : Type u_1} [Ring R] : IsSimpleRing R ↔ Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤