Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-07 14:42 0995ac19

View on Github →

feat(algebra/module): the inverse of a linear map is linear

Estimated changes

added theorem is_linear_map.inverse
added theorem is_submodule.smul_ne_0