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)
:
theorem
IsSimpleRing.of_ringEquiv
{R : Type u_1}
{S : Type u_2}
[NonUnitalNonAssocRing R]
[NonUnitalNonAssocRing S]
(f : R ≃+* S)
(h : IsSimpleRing R)
:
theorem
isSimpleRing_iff_isTwoSided_imp
{R : Type u_1}
[Ring R]
:
IsSimpleRing R ↔ Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤