Commit 2021-02-08 19:30 0c6fa288
View on Github →feat(linear_algebra/basis): if (p : submodule K V) < ⊤, then there exists f : V →ₗ[K] K, p ≤ ker f (#6074)
feat(linear_algebra/basis): if (p : submodule K V) < ⊤, then there exists f : V →ₗ[K] K, p ≤ ker f (#6074)