Commit 2024-02-14 15:41 f0a799f7

View on Github →

feat: connect AddMonoidAlgebra.supDegree and Polynomial.natDegree/degree (#10518)

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

deleted theorem AddMonoidAlgebra.apply_add_of_supDegree_eq

added theorem AddMonoidAlgebra.apply_add_of_supDegree_le

modified def AddMonoidAlgebra.infDegree

added theorem AddMonoidAlgebra.infDegree_withTop_some_comp

modified theorem AddMonoidAlgebra.le_infDegree_add

added theorem AddMonoidAlgebra.supDegree_withBot_some_comp

Modified Mathlib/Data/Polynomial/Degree/Definitions.lean

added theorem Polynomial.supDegree_eq_degree

added theorem Polynomial.supDegree_eq_natDegree

Modified Mathlib/Data/Polynomial/Degree/Lemmas.lean