Theorem Module.exists_set_linearIndependent_of_lt_lift_rank

Modification history

2026-04-15 23:11
Mathlib/LinearAlgebra/Dimension/Basic.lean
feat(Mathlib/LinearAlgebra): embeddings of free modules (#37919) …
Added Module.exists_set_linearIndependent_of_lt_lift_rankView on Github →