Zulip Chat Archive
Stream: maths
Topic: Zero rank modules
Riccardo Brasca (Oct 14 2021 at 15:28):
Does someone see a class more general than no_zero_smul_divisors R M (probably with nontrivial R) that satisfies docs#dim_zero_iff_forall_zero? I really mean a Lean class, to get a reasonable generalization of docs#dim_zero_iff_forall_zero .
Riccardo Brasca (Oct 14 2021 at 16:01):
Last updated: Dec 20 2023 at 11:08 UTC