Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-29 19:07 247dcb2d

View on Github →

feat(linear_algebra): rules for kernel of of_le, cod_restrict, and pair

Estimated changes

Modified src/linear_algebra/basic.lean

added theorem linear_map.ker_cod_restrict

added theorem linear_map.ker_pair

added theorem linear_map.range_cod_restrict

added theorem submodule.ker_of_le