Lean4
/-- Construct an equivalence of rings from homomorphisms in both directions, which are inverses.
-/
@[simps]
def ofHomInv' {R S F G : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [FunLike F R S]
[FunLike G S R] [NonUnitalRingHomClass F R S] [NonUnitalRingHomClass G S R] (hom : F) (inv : G)
(hom_inv_id : (inv : S →ₙ+* R).comp (hom : R →ₙ+* S) = NonUnitalRingHom.id R)
(inv_hom_id : (hom : R →ₙ+* S).comp (inv : S →ₙ+* R) = NonUnitalRingHom.id S) : R ≃+* S
where
toFun := hom
invFun := inv
left_inv := DFunLike.congr_fun hom_inv_id
right_inv := DFunLike.congr_fun inv_hom_id
map_mul' := map_mul hom
map_add' := map_add hom
