Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subsingleton_rat_module

Modification history

2022-08-16 10:36
src/algebra/module/basic.lean
chore(*): restore `subsingleton` instances and remove hacks (#16046) …
Deleted subsingleton_rat_moduleView on Github →
2021-10-08 07:33
src/algebra/module/basic.lean
feat(algebra/module/basic): `module rat E` is a subsingleton (#9570) …
Added subsingleton_rat_moduleView on Github →