Commit 2023-03-29 09:12 6e96221b

View on Github →

feat: port Data.Polynomial.Mirror (#3130)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Mirror.lean

added theorem Polynomial.coeff_mirror

added theorem Polynomial.coeff_mul_mirror

added theorem Polynomial.irreducible_of_mirror

added theorem Polynomial.mirror_C

added theorem Polynomial.mirror_X

added theorem Polynomial.mirror_eq_iff

added theorem Polynomial.mirror_eq_zero

added theorem Polynomial.mirror_eval_one

added theorem Polynomial.mirror_inj

added theorem Polynomial.mirror_involutive

added theorem Polynomial.mirror_leadingCoeff

added theorem Polynomial.mirror_mirror

added theorem Polynomial.mirror_monomial

added theorem Polynomial.mirror_mul_of_domain

added theorem Polynomial.mirror_natDegree

added theorem Polynomial.mirror_natTrailingDegree

added theorem Polynomial.mirror_neg

added theorem Polynomial.mirror_smul

added theorem Polynomial.mirror_trailingCoeff

added theorem Polynomial.mirror_zero

added theorem Polynomial.natDegree_mul_mirror

added theorem Polynomial.natTrailingDegree_mul_mirror