mathlib3

521b8211 - 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)