Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-19 22:45 006b2e70

View on Github →

feat(data/polynomial/reverse): define reverse f, prove that reverse is a multiplicative monoid homomorphism (#4598)

Estimated changes

Created src/data/polynomial/reverse.lean

added theorem polynomial.coeff_reflect

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_support

added theorem polynomial.reflect_zero

added def polynomial.rev_at

added theorem polynomial.rev_at_add

added def polynomial.rev_at_fun

added theorem polynomial.rev_at_fun_eq

added theorem polynomial.rev_at_fun_inj

added theorem polynomial.rev_at_fun_invol

added theorem polynomial.rev_at_invol

added theorem polynomial.rev_at_le

added theorem polynomial.reverse_mul

added theorem polynomial.reverse_mul_of_domain

added theorem polynomial.reverse_zero