Commit 2023-06-08 20:36 e39ba240

View on Github →

feat: port RingTheory.WittVector.MulP (#4869)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/MulP.lean

added theorem WittVector.bind₁_wittMulN_wittPolynomial

added theorem WittVector.mulN_coeff

added theorem WittVector.mulN_isPoly