Theorems · Theorem · functional analysis

RingHomIsometric.inv

∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : SeminormedRing 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂)
  {σ' : 𝕜₂ →+* 𝕜₁} [RingHomInvPair σ σ'] [RingHomIsometric σ], RingHomIsometric σ'

If σ and σ' are mutually inverse, then one is RingHomIsometric if the other is. Not an instance, as it would cause loops.

Defined in

Mathlib.Analysis.Normed.Ring.Lemmas

Cited by

2 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

SeminormedRingSeminormedRingRingHomInvPairRingHomIsometric