Theorem Submodule.codisjoint_iff_exists_add_eq

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) …
Added Submodule.codisjoint_iff_exists_add_eqView on Github →