Theorems · Definition · functional analysis

NormedSpace.restrictScalars

(𝕜 : Type u_1) →
  (𝕜' : Type u_2) →
    (E : Type u_3) →
      [inst : NormedField 𝕜] →
        [inst_1 : NormedField 𝕜'] →
          [NormedAlgebra 𝕜 𝕜'] → [inst_3 : SeminormedAddCommGroup E] → [NormedSpace 𝕜' E] → NormedSpace 𝕜 E

Warning: This declaration should be used judiciously. Please consider using IsScalarTower instead. This definition allows the RestrictScalars.normedSpace instance to be put directly on E rather on RestrictScalars 𝕜 𝕜' E. This would be a very bad instance; both because 𝕜' cannot be inferred, and because it is likely to create instance diamonds. See Note [reducible non-instances].

Defined in

Mathlib.Analysis.Normed.Module.Basic

Cited by

39 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedFieldNormedAlgebraSeminormedAddCommGroupNormedSpace