Commit 2022-02-05 09:51 e78563c0

feat(ring_theory/power_series): reindex trunc of a power series to truncate below index n (#10891) Currently the definition of truncation of a univariate and multivariate power series truncates above the index, that is if we truncate a power series $\sum a_i x^i$ at index n the term $a_n x^n$ is included. This makes it impossible to truncate the first monomial $x^0$ away as it is included with the smallest possible value of n, which causes some issues in applications (imagine if you could only pop elements of lists if the result was non-empty!).