Theorem Submodule.eq_top_iff_forall_basis_mem

Modification history

2025-08-05 16:35
Mathlib/LinearAlgebra/Basis/Basic.lean
feat: basic linear algebra lemmas about matrices (#27605) …
Added Submodule.eq_top_iff_forall_basis_memView on Github →