Commit 2022-05-18 02:13 9f6f605b

View on Github →

feat(data/polynomial/mirror): Central coefficient of p * p.mirror (#14096) This PR adds a lemma (p * p.mirror).coeff (p.nat_degree + p.nat_trailing_degree) = p.sum (λ n, (^ 2)). I also rearranged the file by assumptions on the ring R.

Estimated changes

Modified src/data/polynomial/mirror.lean

added theorem polynomial.coeff_mul_mirror

modified theorem polynomial.irreducible_of_mirror

modified theorem polynomial.mirror_mul_of_domain

modified theorem polynomial.mirror_neg

modified theorem polynomial.mirror_smul