Commit 2025-09-03 08:57 2f4b34ca

View on Github →

feat(SkewMonoidAlgebra): SkewMonoidAlgebra/Support (#27253) Add lemmas regarding the support of a skew monoid algebra.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

Created Mathlib/Algebra/SkewMonoidAlgebra/Support.lean

added theorem SkewMonoidAlgebra.mem_span_support

added theorem SkewMonoidAlgebra.support_mul

added theorem SkewMonoidAlgebra.support_mul_single

added theorem SkewMonoidAlgebra.support_mul_single_eq_image

added theorem SkewMonoidAlgebra.support_mul_single_subset

added theorem SkewMonoidAlgebra.support_neg

added theorem SkewMonoidAlgebra.support_one

added theorem SkewMonoidAlgebra.support_one_subset

added theorem SkewMonoidAlgebra.support_single_mul

added theorem SkewMonoidAlgebra.support_single_mul_eq_image

added theorem SkewMonoidAlgebra.support_single_mul_subset

added theorem SkewMonoidAlgebra.support_single_ne_zero

added theorem SkewMonoidAlgebra.support_single_subset

added theorem SkewMonoidAlgebra.support_sum