Commit 2026-04-15 23:11 dbcdd9f0

View on Github →

feat(Mathlib/LinearAlgebra): embeddings of free modules (#37919)

A free module embeds linearly into any module of strictly greater rank
A free module embeds linearly into another free module iff the other one has greater rank The proofs have been generalised as much as possible.

Estimated changes

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

added theorem Module.Basis.injective_constr_of_linearIndependent

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

added theorem Module.exists_set_linearIndependent_of_lt_lift_rank

added theorem Module.exists_set_linearIndependent_of_lt_rank

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

deleted theorem exists_set_linearIndependent_of_lt_rank

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

added theorem Module.Free.exists_linearMap_injective_of_lift_rank_lt

added theorem Module.Free.exists_linearMap_injective_of_linearIndependent_of_lift_rank_le

added theorem Module.Free.exists_linearMap_injective_of_linearIndependent_of_rank_le

added theorem Module.Free.exists_linearMap_injective_of_rank_lt

added theorem finrank_le_iff_exists_linearMap

added theorem lift_rank_le_iff_exists_linearMap

added theorem rank_le_iff_exists_linearMap