mathlib3

7b1ce10b - fix(analysis/normed_space/basic): add an alias instance to fix an inference issue (#8547)

fix(analysis/normed_space/basic): add an alias instance to fix an inference issue (#8547) This adds an instance from [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20resolution.20under.20binders/near/245176934).