Theorems · Theorem · ring theory

RingEquiv.ofBijective_symm_comp

∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R →ₙ+* S) (hf : Function.Bijective ⇑f), (↑(RingEquiv.ofBijective f hf).symm).comp f = NonUnitalRingHom.id R

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring