Transfer normed algebraic structures from α to Shrink α

instance Shrink.instSeminormedAddCommGroup {α : Type u_3} [Small.{v, u_3} α] [SeminormedAddCommGroup α] : SeminormedAddCommGroup (Shrink.{v, u_3} α)

Equations

• Shrink.instSeminormedAddCommGroup = (equivShrink α).symm.seminormedAddCommGroup

instance Shrink.instNormedAddCommGroup {α : Type u_3} [Small.{v, u_3} α] [NormedAddCommGroup α] : NormedAddCommGroup (Shrink.{v, u_3} α)

Equations

• Shrink.instNormedAddCommGroup = (equivShrink α).symm.normedAddCommGroup

instance Shrink.instNormedSpace {𝕜 : Type u_2} {α : Type u_3} [Small.{v, u_3} α] [NormedField 𝕜] [SeminormedAddCommGroup α] [NormedSpace 𝕜 α] : NormedSpace 𝕜 (Shrink.{v, u_3} α)

Equations

• Shrink.instNormedSpace = Equiv.normedSpace 𝕜 (equivShrink α).symm