Commit 2020-04-13 05:19 51f7319b
View on Github →chore(algebra/module): rename type vars, minor cleanup, add module docstring (#2392)
- Use
R
,S
for rings,k
for a field,M
,M₂
etc for modules; - Add a
semiring
version ofring_hom.to_module
; - Stop using
{rα : ring α}
trick as Lean 3.7 tries unification before class search; - Add a short module docstring