Commit 2025-07-08 15:32 0ce5741d

feat(LinearAlgebra/Span/Defs): replace Submodule.exists_add_eq_of_codisjoint with an iff (#26796) Instead of introducing another theorem to go the other way, I have upgraded this one to an iff. The changed order of terms is preferable in my application (and probably others) because to prove the existential it is enough to provide the two witnesses first and leave everything else to simp.