Documentation

Mathlib.Analysis.Normed.Module.Shrink

Transfer normed algebraic structures from α to Shrink α #

source
🔸 coverage
instance Shrink.instSeminormedAddCommGroup {α : Type u_3} [Small.{v, u_3} α] [SeminormedAddCommGroup α] :
SeminormedAddCommGroup (Shrink.{v, u_3} α)
Equations
    source
    🔸 coverage
    instance Shrink.instNormedAddCommGroup {α : Type u_3} [Small.{v, u_3} α] [NormedAddCommGroup α] :
    NormedAddCommGroup (Shrink.{v, u_3} α)
    Equations
      source
      🔸 coverage
      instance Shrink.instNormedSpace {𝕜 : Type u_2} {α : Type u_3} [Small.{v, u_3} α] [NormedField 𝕜] [SeminormedAddCommGroup α] [NormedSpace 𝕜 α] :
      NormedSpace 𝕜 (Shrink.{v, u_3} α)
      Equations