Theorem Submodule.span_range_update_add_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_add_smulView on Github →