Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_independent.image_of_comp

Modification history

2021-04-06 05:50
src/linear_algebra/linear_independent.lean
feat(linear_algebra): `c ≤ dim K E` iff there exists a linear independent `s : set E`, `card s = c` (#7014)
Added linear_independent.image_of_compView on Github →