feat(data/polynomial/basic): monomial_left_inj (#6430)
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)





leanprover-community/mathlib,leanprover-community/mathlib