Theorems · Definition · functional analysis

NonUnitalNormedCommRing.induced

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

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

Defined in

Mathlib.Analysis.Normed.Ring.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeNonUnitalCommRingNonUnitalNormedCommRingNonUnitalRingHomClass