Commit 2023-06-28 16:07 b47e7d28

View on Github →

feat: port RingTheory.WittVector.MulCoeff (#5554)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/WittVector/Frobenius.lean

Modified Mathlib/RingTheory/WittVector/InitTail.lean

Modified Mathlib/RingTheory/WittVector/IsPoly.lean

Created Mathlib/RingTheory/WittVector/MulCoeff.lean

added theorem WittVector.mul_polyOfInterest_aux1

added theorem WittVector.mul_polyOfInterest_aux2

added theorem WittVector.mul_polyOfInterest_aux3

added theorem WittVector.mul_polyOfInterest_aux4

added theorem WittVector.mul_polyOfInterest_aux5

added theorem WittVector.mul_polyOfInterest_vars

added def WittVector.nthRemainder

added theorem WittVector.nthRemainder_spec

added theorem WittVector.nth_mul_coeff'

added theorem WittVector.nth_mul_coeff

added theorem WittVector.peval_polyOfInterest'

added theorem WittVector.peval_polyOfInterest

added def WittVector.polyOfInterest

added theorem WittVector.polyOfInterest_vars

added theorem WittVector.polyOfInterest_vars_eq

added def WittVector.remainder

added theorem WittVector.remainder_vars

added def WittVector.wittPolyProd

added def WittVector.wittPolyProdRemainder

added theorem WittVector.wittPolyProdRemainder_vars

added theorem WittVector.wittPolyProd_vars

Modified Mathlib/RingTheory/WittVector/WittPolynomial.lean

added theorem wittPolynomial_eq_sum_C_mul_X_pow

deleted theorem wittPolynomial_eq_sum_c_mul_x_pow