of_surjective — Mathlib

English

Let f: R → S be a surjective ring homomorphism with R simple; then S is simple.

Русский

Пусть f: R → S — сюръективный гомоморфизм колец, и R простое; тогда S простое.

LaTeX

$$If f: R →+* S is surjective and IsSimpleRing R, then IsSimpleRing S.$$

Lean4

theorem of_surjective {R S : Type*} [NonAssocRing R] [NonAssocRing S] [Nontrivial S] (f : R →+* S) (h : IsSimpleRing R)
    (hf : Function.Surjective f) : IsSimpleRing S where
  simple := OrderIso.isSimpleOrder (RingEquiv.ofBijective f ⟨RingHom.injective f, hf⟩).symm.mapTwoSidedIdeal

Похожие утверждения