Commit 2021-03-05 20:52 626cb422

View on Github →

feat(data/polynomial/mirror): new file (#6426) This files defines an alternate version of polynomial.reverse. This version is often nicer to work with since it preserves nat_degree and nat_trailing_degree and is always an involution. (this PR is part of the irreducibility saga)

Estimated changes

Created src/data/polynomial/mirror.lean

added theorem polynomial.coeff_mirror

added theorem polynomial.irreducible_of_mirror

added theorem polynomial.mirror_C

added theorem polynomial.mirror_X

added theorem polynomial.mirror_eq_zero

added theorem polynomial.mirror_eval_one

added theorem polynomial.mirror_leading_coeff

added theorem polynomial.mirror_mirror

added theorem polynomial.mirror_monomial

added theorem polynomial.mirror_mul_of_domain

added theorem polynomial.mirror_nat_degree

added theorem polynomial.mirror_nat_trailing_degree

added theorem polynomial.mirror_neg

added theorem polynomial.mirror_smul

added theorem polynomial.mirror_trailing_coeff

added theorem polynomial.mirror_zero