Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-11 00:42 f67df78c

View on Github →

chore(algebra/module): add some missing *_cast tags (#1863)

Estimated changes

modified theorem submodule.coe_add
modified theorem submodule.coe_neg
modified theorem submodule.coe_smul
modified theorem submodule.coe_sub
modified theorem submodule.coe_zero