Theorems · Definition · ring theory

RingEquiv.ofRingHom

{R : Type u_4} →
  {S : Type u_5} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] →
        (f : R →+* S) → (g : S →+* R) → f.comp g = RingHom.id S → g.comp f = RingHom.id R → R ≃+* S

If a ring homomorphism has an inverse, it is a ring isomorphism.

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

9 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

NonAssocSemiringNonAssocSemiring