English
If σ is a RingIsometric and σ' is its inverse, then σ' is also a RingIsometric.
Русский
Если σ является изометрией круга, и σ' — его обратная, то σ' тоже является изометрией.
LaTeX
$$$ \\text{If } \\sigma: A \\to B \\text{ is isometric and } \\sigma' = \\sigma^{-1}, \\text{ then } \\sigma' \\text{ is isometric.}$$$
Lean4
/-- If `σ` and `σ'` are mutually inverse, then one is `RingHomIsometric` if the other is. Not an
instance, as it would cause loops. -/
theorem inv {𝕜₁ 𝕜₂ : Type*} [SeminormedRing 𝕜₁] [SeminormedRing 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {σ' : 𝕜₂ →+* 𝕜₁}
[RingHomInvPair σ σ'] [RingHomIsometric σ] : RingHomIsometric σ' :=
⟨fun {x} ↦ by rw [← RingHomIsometric.norm_map (σ := σ), RingHomInvPair.comp_apply_eq₂]⟩
