Theorem SkewMonoidAlgebra.update_zero_eq_erase

Modification history

2025-09-19 07:04
Mathlib/Algebra/SkewMonoidAlgebra/Single.lean
chore(*): drop some `Decidable`/`Fintype` assumptions (#29785) …
Modified SkewMonoidAlgebra.update_zero_eq_eraseView on Github →
2025-09-16 12:06
Mathlib/Algebra/SkewMonoidAlgebra/Single.lean
feat(SkewMonoidAlgebra): Modifying elements of skew monoid algebra at exactly one point (erase and update) (#29319) …
Added SkewMonoidAlgebra.update_zero_eq_eraseView on Github →