Commit 2024-02-13 21:51 7a752844

View on Github →

feat: extend AddMonoidAlgebra.supDegree API (#10355) This is a part of #7173 that I hope will be uncontroversial.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

added theorem AddMonoidAlgebra.apply_add_of_supDegree_eq

added theorem AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree

added theorem AddMonoidAlgebra.ne_zero_of_not_supDegree_le

added theorem AddMonoidAlgebra.ne_zero_of_supDegree_ne_bot

modified theorem AddMonoidAlgebra.supDegree_add_le

modified theorem AddMonoidAlgebra.supDegree_mul_le

added theorem AddMonoidAlgebra.supDegree_neg

added theorem AddMonoidAlgebra.supDegree_prod_le

added theorem AddMonoidAlgebra.supDegree_single

added theorem AddMonoidAlgebra.supDegree_single_ne_zero

added theorem AddMonoidAlgebra.supDegree_sub_le

added theorem AddMonoidAlgebra.supDegree_sum_le

added theorem AddMonoidAlgebra.supDegree_zero