Theorems · Theorem · ring theory

RingEquiv.ofRingHom_apply

∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (g : S →+* R)
  (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R) (a : R), (RingEquiv.ofRingHom f g h₁ h₂) a = f a

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

8 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiring