Commit 2023-03-09 08:04 0b15aefc

View on Github →

feat: port Data.Polynomial.Reverse (#2729)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Reverse.lean

added theorem Polynomial.coeff_one_reverse

added theorem Polynomial.coeff_reflect

added theorem Polynomial.coeff_reverse

added theorem Polynomial.coeff_zero_reverse

added theorem Polynomial.eval₂_reflect_eq_zero_iff

added theorem Polynomial.eval₂_reflect_mul_pow

added theorem Polynomial.eval₂_reverse_eq_zero_iff

added theorem Polynomial.eval₂_reverse_mul_pow

added theorem Polynomial.natDegree_eq_reverse_natDegree_add_natTrailingDegree

added theorem Polynomial.reflect_C

added theorem Polynomial.reflect_C_mul

added theorem Polynomial.reflect_C_mul_X_pow

added theorem Polynomial.reflect_add

added theorem Polynomial.reflect_eq_zero_iff

added theorem Polynomial.reflect_monomial

added theorem Polynomial.reflect_mul

added theorem Polynomial.reflect_mul_induction

added theorem Polynomial.reflect_neg

added theorem Polynomial.reflect_sub

added theorem Polynomial.reflect_support

added theorem Polynomial.reflect_zero

added def Polynomial.revAt

added def Polynomial.revAtFun

added theorem Polynomial.revAtFun_eq

added theorem Polynomial.revAtFun_inj

added theorem Polynomial.revAtFun_invol

added theorem Polynomial.revAt_add

added theorem Polynomial.revAt_invol

added theorem Polynomial.revAt_le

added theorem Polynomial.revAt_zero

added theorem Polynomial.reverse_eq_zero

added theorem Polynomial.reverse_leadingCoeff

added theorem Polynomial.reverse_mul

added theorem Polynomial.reverse_mul_of_domain

added theorem Polynomial.reverse_natDegree

added theorem Polynomial.reverse_natDegree_le

added theorem Polynomial.reverse_natTrailingDegree

added theorem Polynomial.reverse_neg

added theorem Polynomial.reverse_trailingCoeff

added theorem Polynomial.reverse_zero

added theorem Polynomial.trailingCoeff_mul