Transfer normed algebraic structures from α to Shrink α

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• Shrink.instNormedSpace = { toMulAction := Shrink.instMulAction, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯, norm_smul_le := ⋯ }