Theorems · Definition · functional analysis

AlgebraNorm.isScalarTower_restriction

{R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} →
      [inst_1 : Ring S] →
        [inst_2 : Algebra R S] →
          {A : Type u_3} →
            [inst_3 : CommRing A] →
              [inst_4 : Algebra R A] →
                [inst_5 : Algebra A S] →
                  [IsScalarTower R A S] → Function.Injective ⇑(algebraMap A S) → AlgebraNorm R S → AlgebraNorm R A

The restriction of an algebra norm in a scalar tower.

Defined in

Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedCommRingRingAlgebraCommRingAlgebraAlgebraIsScalarTower