Theorems · Inductive type · functional analysis

RingHomIsometric

{R₁ : Type u_5} →
  {R₂ : Type u_6} → [inst : Semiring R₁] → [inst_1 : Semiring R₂] → [Norm R₁] → [Norm R₂] → (R₁ →+* R₂) → Prop

This class states that a ring homomorphism is isometric. This is a sufficient assumption for a continuous semilinear map to be bounded and this is the main use for this typeclass.

Defined in

Mathlib.Analysis.Normed.Ring.Basic

Cited by

282 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 82 definitions · uses no axioms

Assumes

SemiringSemiringNormNorm