Theorem Submodule.span_range_update_sub_smul

Modification history

2024-12-29 20:43
Mathlib/LinearAlgebra/Span/Defs.lean
feat: quotienting out a polynomial in a family doesn't change the span (#20297) …
Added Submodule.span_range_update_sub_smulView on Github →