mathlib

0e095f0e - feat(data/polynomial/mirror): `mirror` is injective (#14254)

feat(data/polynomial/mirror): `mirror` is injective (#14254) This PR adds an `inj` lemma for `mirror`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>