Theorems · Definition · ring theory

NonUnitalRingHom.inverse

{R : Type u_4} →
  {S : Type u_5} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        (f : R →ₙ+* S) → (g : S → R) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → S →ₙ+* R

makes a NonUnitalRingHom from the bijective inverse of a NonUnitalRingHom

Defined in: Mathlib.Algebra.Ring.Equiv
Cited by: 1 results in Mathlib
Foundations: Depth 16 from the axioms · uses no axioms
Assumes: NonUnitalNonAssocSemiring NonUnitalNonAssocSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
AddMonoidHomproof · cited by 3,230
NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
MulHomproof · cited by 299
AddMonoidHomClass.toAddMonoidHomproof · cited by 232
NonUnitalRingHomstatement and proof · cited by 157
MulHomClass.toMulHomproof · cited by 31
MulHom.inverseproof · cited by 3
AddMonoidHom.inverseproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

NonUnitalRingHom.inverse_applystatement and proof · cited by 0