Zero rank modules

Stream: maths

[Riccardo Brasca]

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]

#9713