Commit 2023-03-08 14:42 684fd0e2

View on Github →

feat: port Algebra.MonoidAlgebra.Support (#2720)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/MonoidAlgebra/Support.lean

added theorem AddMonoidAlgebra.mem_span_support'

added theorem AddMonoidAlgebra.mem_span_support

added theorem AddMonoidAlgebra.support_mul

added theorem AddMonoidAlgebra.support_mul_single

added theorem AddMonoidAlgebra.support_single_mul

added theorem MonoidAlgebra.mem_span_support

added theorem MonoidAlgebra.support_mul

added theorem MonoidAlgebra.support_mul_single

added theorem MonoidAlgebra.support_mul_single_eq_image

added theorem MonoidAlgebra.support_mul_single_subset

added theorem MonoidAlgebra.support_single_mul

added theorem MonoidAlgebra.support_single_mul_eq_image

added theorem MonoidAlgebra.support_single_mul_subset