Theorems · Definition · functional analysis

NormedRing.induced

{F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : Ring R] →
          [inst_2 : NormedRing S] → [NonUnitalRingHomClass F R S] → (f : F) → Function.Injective ⇑f → NormedRing R

An injective non-unital ring homomorphism from a Ring to a NormedRing induces a NormedRing structure on the domain. See note [reducible non-instances]

Defined in

Mathlib.Analysis.Normed.Ring.Basic

Cited by

0 results in Mathlib

Foundations

Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FunLikeRingNormedRingNonUnitalRingHomClass