Commit 2025-08-14 21:19 3d1b2611

View on Github →

feat(SkewMonoidAlgebra): coeff_mul lemmas (#27255) Add lemmas regarding the interaction of multiplication and the SkewMonoidAlgebra.coeff.

Estimated changes

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

added theorem SkewMonoidAlgebra.coeff_mul

added theorem SkewMonoidAlgebra.coeff_mul_antidiagonal_finsum

added theorem SkewMonoidAlgebra.coeff_mul_antidiagonal_of_finset

added theorem SkewMonoidAlgebra.coeff_mul_left

added theorem SkewMonoidAlgebra.coeff_mul_right

added theorem SkewMonoidAlgebra.coeff_mul_single

added theorem SkewMonoidAlgebra.coeff_mul_single_aux

added theorem SkewMonoidAlgebra.coeff_mul_single_of_not_exists_mul

added theorem SkewMonoidAlgebra.coeff_mul_single_one

added theorem SkewMonoidAlgebra.coeff_single_mul

added theorem SkewMonoidAlgebra.coeff_single_mul_aux

added theorem SkewMonoidAlgebra.coeff_single_mul_of_not_exists_mul

added theorem SkewMonoidAlgebra.coeff_single_one_mul