Zulip Chat Archive
Stream: Is there code for X?
Topic: zero module
Kevin Buzzard (Jan 19 2023 at 18:57):
Do we have a way of saying M = 0 if module M R? More generally I could ask the same question for abelian groups I guess. Is it just subsingleton M?
Johan Commelin (Jan 19 2023 at 18:58):
I think subsingleton is fine
Eric Wieser (Jan 19 2023 at 19:58):
If you want the zero module you can use unit
Kevin Buzzard (Jan 19 2023 at 20:23):
My question is about _a_ zero module. Is unit an R-module BTW?
Jireh Loreaux (Jan 19 2023 at 20:55):
It shouldn't be right? Because R would be a metavariable in the instance.
Mario Carneiro (Jan 19 2023 at 21:29):
I think R is not an out-param so this should be fine
Riccardo Brasca (Jan 19 2023 at 21:50):
I remember a discussion about the fact that the 0-module is free, and I also thought it was a dangerous instance, but it's not. When Lean is looking for the instance module R unit it knows R.
Riccardo Brasca (Jan 19 2023 at 21:51):
Eric Wieser (Jan 19 2023 at 22:48):
Last updated: Dec 20 2023 at 11:08 UTC