Zulip Chat Archive

Stream: maths

Topic: Normed algebras

view this post on Zulip Yury G. Kudryashov (Jan 08 2020 at 01:45):

I started thinking about formalizing normed algebras. What is the best way to avoid diamonds to module through algebra (path 1) and normed_space (path 2)? Extend algebra and define coercion to normed space? Something else?

Last updated: May 06 2021 at 17:38 UTC