Commit 2023-03-15 22:17 a1e0e208

View on Github →

feat: port Algebra.MonoidAlgebra.Degree (#2918)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/MonoidAlgebra/Degree.lean

added theorem AddMonoidAlgebra.le_inf_support_add

added theorem AddMonoidAlgebra.le_inf_support_finset_prod

added theorem AddMonoidAlgebra.le_inf_support_list_prod

added theorem AddMonoidAlgebra.le_inf_support_mul

added theorem AddMonoidAlgebra.le_inf_support_multiset_prod

added theorem AddMonoidAlgebra.le_inf_support_pow

added theorem AddMonoidAlgebra.sup_support_add_le

added theorem AddMonoidAlgebra.sup_support_finset_prod_le

added theorem AddMonoidAlgebra.sup_support_list_prod_le

added theorem AddMonoidAlgebra.sup_support_mul_le

added theorem AddMonoidAlgebra.sup_support_multiset_prod_le

added theorem AddMonoidAlgebra.sup_support_pow_le