Theorem Module.Free.exists_linearMap_injective_of_linearIndependent_of_rank_le

Modification history

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