English
From a ring isomorphism e: R1 ≃+* R2, the forward and inverse ring homomorphisms form an inverse pair.
Русский
Из кольцевого изоморфизма e: R1 ≃+* R2 получаются взаимно обратные кольцевые гомоморфизмы, образующие обратную пару.
LaTeX
$$$\text{RingHomInvPair}(\text{toRingHom}(e), \text{toRingHom}(e)^{-1})$$$
Lean4
/-- Construct a `RingHomInvPair` from both directions of a ring equiv.
This is not an instance, as for equivalences that are involutions, a better instance
would be `RingHomInvPair e e`. Indeed, this declaration is not currently used in mathlib.
-/
theorem of_ringEquiv (e : R₁ ≃+* R₂) : RingHomInvPair (↑e : R₁ →+* R₂) ↑e.symm :=
⟨e.symm_toRingHom_comp_toRingHom, e.symm.symm_toRingHom_comp_toRingHom⟩
