Commit 2023-05-22 18:01 06326c9c

View on Github →

feat: port RingTheory.WittVector.WittPolynomial (#3355)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/WittPolynomial.lean

added theorem aeval_wittPolynomial

added theorem bind₁_wittPolynomial_xInTermsOfW

added theorem bind₁_xInTermsOfW_wittPolynomial

added theorem constantCoeff_wittPolynomial

added theorem constantCoeff_xInTermsOfW

added theorem map_wittPolynomial

added theorem wittPolynomial_eq_sum_c_mul_x_pow

added theorem wittPolynomial_one

added theorem wittPolynomial_vars

added theorem wittPolynomial_vars_subset

added theorem wittPolynomial_zMod_self

added theorem wittPolynomial_zero

added theorem xInTermsOfW_aux

added theorem xInTermsOfW_eq

added theorem xInTermsOfW_vars_aux

added theorem xInTermsOfW_vars_subset

added theorem xInTermsOfW_zero