Theorem Submodule.mapsTo_span

Modification history

2025-12-27 09:40
Mathlib/LinearAlgebra/Span/Basic.lean
chore(*): restrict operations to `LinearMap`s (#33241) …
Modified Submodule.mapsTo_spanView on Github →
2025-05-02 12:26
Mathlib/LinearAlgebra/Span/Basic.lean
feat(Span/Basic): add `Submodule.mapsTo_span` (#24462) …
Added Submodule.mapsTo_spanView on Github →