Zulip Chat Archive
Stream: maths
Topic: monoid and smul for seminorms
Moritz Doll (Jan 12 2022 at 21:15):
Hi, I want to implement add_comm_monoid and mul_action over nnreal for seminorms, is there something to be aware of? the docs mentioned some issues with nsmul.
Heather Macbeth (Jan 12 2022 at 21:23):
Can you just use module nnreal? I.e., mathlib allows you to take a module over a semiring.
Eric Wieser (Jan 12 2022 at 22:38):
Why don't you start with the PR for mul_action?
Moritz Doll (Jan 12 2022 at 22:43):
ok, I will do that
Eric Wieser (Jan 12 2022 at 22:43):
Or even for has_add at the same time. Once you have both, docs#function.injective.add_monoid_smul will trivially give you the full structure
Eric Wieser (Jan 12 2022 at 22:45):
(got the link right in the end)
Moritz Doll (Jan 13 2022 at 00:45):
Last updated: Dec 20 2023 at 11:08 UTC