Zulip Chat Archive

Stream: maths

Topic: Normed algebras

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: Dec 20 2023 at 11:08 UTC