Commit 2023-12-17 20:09 07b02ce3

View on Github →

feat(Algebra/MonoidAlgebra): when single and of commute (#8975) Also removes an autoImplicit that tripped me up when working on this file.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

added theorem AddMonoidAlgebra.of'_commute

added theorem AddMonoidAlgebra.single_commute_single

modified theorem AddMonoidAlgebra.sum_single_index

added theorem MonoidAlgebra.of_commute

added theorem MonoidAlgebra.single_commute

added theorem MonoidAlgebra.single_commute_single

modified theorem MonoidAlgebra.sum_single_index