Theorem Submodule.exists_le_ker_of_not_mem

Modification history

2025-05-25 12:30

Mathlib/LinearAlgebra/Basis/VectorSpace.lean

chore(*): not_mem/nmem -> notMem (#25159)

Deleted Submodule.exists_le_ker_of_not_mem View on Github →

2025-05-07 13:32

Mathlib/LinearAlgebra/Basis/VectorSpace.lean

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

Added Submodule.exists_le_ker_of_not_mem View on Github →