Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-05 14:35 88202b6c

View on Github →

refactor(algebra/module): clean up is_submodule projections

Estimated changes

Modified algebra/module.lean

added theorem is_submodule.add

modified theorem is_submodule.add_val

modified theorem is_submodule.neg

modified theorem is_submodule.neg_val

modified theorem is_submodule.sub

added theorem is_submodule.sub_val

added theorem is_submodule.sum

added theorem is_submodule.zero