Theorems · Definition · functional analysis

NonUnitalSeminormedRing.induced

{F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : NonUnitalRing R] →
          [inst_2 : NonUnitalSeminormedRing S] → [NonUnitalRingHomClass F R S] → F → NonUnitalSeminormedRing R

A non-unital ring homomorphism from a NonUnitalRing to a NonUnitalSeminormedRing induces a NonUnitalSeminormedRing structure on the domain. See note [reducible non-instances]

Defined in

Mathlib.Analysis.Normed.Ring.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeNonUnitalRingNonUnitalSeminormedRingNonUnitalRingHomClass