of_ringEquiv — Mathlib

English

If there is a ring isomorphism e: R ≃+* S, then IsSimpleRing R ⇔ IsSimpleRing S.

Русский

Если существует изоморфизм колец e: R ≃+* S, то IsSimpleRing R эквивалентно IsSimpleRing S.

LaTeX

$$IsSimpleRing R ↔ IsSimpleRing S when R ≃+* S.$$

Lean4

theorem of_ringEquiv {R S : Type*} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R ≃+* S)
    (h : IsSimpleRing R) : IsSimpleRing S where simple := OrderIso.isSimpleOrder f.symm.mapTwoSidedIdeal

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