Theorems · Definition · functional analysis

Seminorm.restrictScalars

(𝕜 : Type u_3) →
  {E : Type u_7} →
    {𝕜' : Type u_12} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedRing 𝕜'] →
          [inst_2 : SMul 𝕜 𝕜'] →
            [NormSMulClass 𝕜 𝕜'] →
              [NormOneClass 𝕜'] →
                [inst_5 : AddCommGroup E] →
                  [inst_6 : Module 𝕜' E] → [inst_7 : SMul 𝕜 E] → [IsScalarTower 𝕜 𝕜' E] → Seminorm 𝕜' E → Seminorm 𝕜 E

Reinterpret a seminorm over a field 𝕜' as a seminorm over a smaller field 𝕜. This will typically be used with RCLike 𝕜' and 𝕜 = ℝ.

Defined in

Mathlib.Analysis.Seminorm

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedFieldSeminormedRingSMulNormSMulClassNormOneClassAddCommGroupModuleSMulIsScalarTower