Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-20 01:48 a5878bbe

View on Github →

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

Estimated changes

Modified src/data/polynomial/mirror.lean

added theorem polynomial.mirror_eq_iff

modified theorem polynomial.mirror_eq_zero

added theorem polynomial.mirror_involutive

modified theorem polynomial.mirror_leading_coeff

modified theorem polynomial.mirror_trailing_coeff