Commit 2023-08-14 05:39 c769b9d8

View on Github →

feat: add definitions of degrees of AddMonoidAlgebras (#6260) This PR defines

  1. the supDegree of an AddMonoidAlgebra, graded by a SemilatticeSup;
  2. the infDegree of an AddMonoidAlgebra, graded by a SemilatticeInf;
  3. the maxDegree of an AddMonoidAlgebra, graded by a LinearOrder with a bottom element;
  4. the minDegree of an AddMonoidAlgebra, graded by a LinearOrder with a top element. It also proves that under addition and multiplication in the AddMonoidAlgebra, each degree behaves as expected. The lemmas are there simply to give a sample usage of the new definition. The corresponding mathlib3 PR was not-too-late and closed unmerged.

Estimated changes