Commit 2025-05-07 13:32 8b369e07

View on Github →

chore(Basis): split Submodule.exists_le_ker_of_lt_top (#23233)

Estimated changes

Modified Mathlib/LinearAlgebra/Basis/VectorSpace.lean

added theorem LinearMap.exists_extend_of_not_mem

added theorem Submodule.exists_le_ker_of_not_mem