Commit 2023-06-05 10:42 3452e3d3

View on Github →

feat: port RingTheory.WittVector.Defs (#4687)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/Defs.lean

added theorem WittVector.add_coeff

added theorem WittVector.add_coeff_zero

added theorem WittVector.coeff_mk

added theorem WittVector.constantCoeff_wittAdd

added theorem WittVector.constantCoeff_wittMul

added theorem WittVector.constantCoeff_wittNSMul

added theorem WittVector.constantCoeff_wittNeg

added theorem WittVector.constantCoeff_wittSub

added theorem WittVector.constantCoeff_wittZSMul

added def WittVector.eval

added theorem WittVector.ext

added theorem WittVector.ext_iff

added def WittVector.mk

added theorem WittVector.mul_coeff

added theorem WittVector.mul_coeff_zero

added theorem WittVector.neg_coeff

added theorem WittVector.nsmul_coeff

added theorem WittVector.one_coeff_eq_of_pos

added theorem WittVector.one_coeff_zero

added def WittVector.peval

added theorem WittVector.pow_coeff

added theorem WittVector.sub_coeff

added theorem WittVector.v2_coeff

added def WittVector.wittAdd

added theorem WittVector.wittAdd_vars

added theorem WittVector.wittAdd_zero

added def WittVector.wittMul

added theorem WittVector.wittMul_vars

added theorem WittVector.wittMul_zero

added def WittVector.wittNSMul

added theorem WittVector.wittNSMul_vars

added def WittVector.wittNeg

added theorem WittVector.wittNeg_vars

added theorem WittVector.wittNeg_zero

added def WittVector.wittOne

added theorem WittVector.wittOne_pos_eq_zero

added theorem WittVector.wittOne_zero_eq_one

added def WittVector.wittPow

added theorem WittVector.wittPow_vars

added def WittVector.wittSub

added theorem WittVector.wittSub_vars

added theorem WittVector.wittSub_zero

added def WittVector.wittZSMul

added theorem WittVector.wittZSMul_vars

added def WittVector.wittZero

added theorem WittVector.wittZero_eq_zero

added theorem WittVector.zero_coeff

added theorem WittVector.zsmul_coeff

added structure WittVector