Commit 2024-12-29 20:43 3f703ecb

View on Github →

feat: quotienting out a polynomial in a family doesn't change the span (#20297) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Algebra/Polynomial/CoeffMem.lean

added theorem Polynomial.idealSpan_range_update_divByMonic

Modified Mathlib/LinearAlgebra/Span/Defs.lean

added theorem Submodule.span_range_update_add_smul

added theorem Submodule.span_range_update_sub_smul

modified theorem Submodule.sup_toAddSubgroup