mirror): `mirror_eq_iff` (#14238)

Commit

3 years ago

feat(data/polynomial/mirror): `mirror_eq_iff` (#14238) This PR adds a lemma stating that `p.mirror = q ↔ p = q.mirror`.

Author

tb65536

Parents