Theorem Submodule.image_span_subset

Modification history

2025-12-27 09:40
Mathlib/LinearAlgebra/Span/Basic.lean
chore(*): restrict operations to `LinearMap`s (#33241) …
Modified Submodule.image_span_subsetView on Github →
2024-01-31 20:39
Mathlib/LinearAlgebra/Span.lean
feat: add `Submodule.image_span_subset(_span)` and golf (#10017) …
Added Submodule.image_span_subsetView on Github →