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: May 02 2025 at 03:31 UTC