Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-16 15:21 ba5d1f63

View on Github →

feat(linear_algebra/basic): add comap span lemmas (#5744) We already had map_span but nothing for comap.

Estimated changes

modified theorem linear_map.disjoint_ker'
modified theorem linear_map.ker_eq_bot
added theorem linear_map.ker_le_iff
modified theorem linear_map.range_prod_eq
modified theorem linear_map.sub_mem_ker_iff