Commit 2021-02-26 00:42 521b8211
View on Github →feat(data/polynomial/basic): monomial_left_inj (#6430)
A version of finsupp.single_left_inj for monomials, so that it works with rw.
(this PR is part of the irreducibility saga)
feat(data/polynomial/basic): monomial_left_inj (#6430)
A version of finsupp.single_left_inj for monomials, so that it works with rw.
(this PR is part of the irreducibility saga)