Theorem Submodule.exists_add_eq_of_codisjoint
Modification history
2025-07-08 15:32
Mathlib/LinearAlgebra/Span/Defs.lean
feat(LinearAlgebra/Span/Defs): replace Submodule.exists_add_eq_of_codisjoint with an iff (#26796) …
Deleted Submodule.exists_add_eq_of_codisjointView on Github →