Commit 2025-04-01 08:50 4a16cda1

View on Github →

feat(Algebra/MonoidAlgebra/Defs): add simple lemmas about single (#22982) This PR adds a couple of lemmas about single (for MonoidAlgebra, Finsupp, DFinsupp and Pi). Note that these aren't simp lemmas since simp can already prove them.

Estimated changes

Modified Mathlib/Algebra/Group/Pi/Basic.lean

added theorem Pi.mulSingle_eq_one_iff

added theorem Pi.mulSingle_ne_one_iff

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

added theorem AddMonoidAlgebra.single_ne_zero

added theorem MonoidAlgebra.single_ne_zero

Modified Mathlib/Data/DFinsupp/Defs.lean

added theorem DFinsupp.single_ne_zero

Modified Mathlib/Data/Finsupp/Single.lean

added theorem Finsupp.single_ne_zero