Commit 2025-09-16 12:06 3b67fc96

View on Github →

feat(SkewMonoidAlgebra): Modifying elements of skew monoid algebra at exactly one point (erase and update) (#29319) Basic results on updating/erasing an element of a skew monoid algebras using one point of the domain. Similar to Finsupp.erase and Finsupp.update

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/SkewMonoidAlgebra/Single.lean

added theorem SkewMonoidAlgebra.coeff_erase_apply

added theorem SkewMonoidAlgebra.coeff_erase_ne

added theorem SkewMonoidAlgebra.coeff_erase_same

added theorem SkewMonoidAlgebra.coeff_update

added theorem SkewMonoidAlgebra.coeff_update_apply

added theorem SkewMonoidAlgebra.coeff_update_ne

added theorem SkewMonoidAlgebra.coeff_update_same

added def SkewMonoidAlgebra.erase

added theorem SkewMonoidAlgebra.erase_single

added theorem SkewMonoidAlgebra.induction

added theorem SkewMonoidAlgebra.single_add_erase

added theorem SkewMonoidAlgebra.support_erase

added theorem SkewMonoidAlgebra.support_update

added def SkewMonoidAlgebra.update

added theorem SkewMonoidAlgebra.update_eq_erase_add_single

added theorem SkewMonoidAlgebra.update_self

added theorem SkewMonoidAlgebra.update_zero_eq_erase

added theorem SkewMonoidAlgebra.zero_update