Commit 2023-06-27 11:58 64ec3a13

View on Github →

feat: port RingTheory.WittVector.Verschiebung (#4897)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/RingTheory/WittVector/IsPoly.lean

deleted theorem WittVector.IsPoly.comp

deleted theorem WittVector.IsPoly.comp₂

deleted theorem WittVector.IsPoly₂.comp

modified theorem WittVector.IsPoly₂.compLeft

modified theorem WittVector.IsPoly₂.compRight

deleted theorem WittVector.IsPoly₂.diag

deleted theorem WittVector.addIsPoly₂

deleted theorem WittVector.mulIsPoly₂

deleted theorem WittVector.negIsPoly

Created Mathlib/RingTheory/WittVector/Verschiebung.lean

added theorem WittVector.aeval_verschiebungPoly

added theorem WittVector.aeval_verschiebung_poly'

added theorem WittVector.bind₁_verschiebungPoly_wittPolynomial

added theorem WittVector.ghostComponent_verschiebung

added theorem WittVector.ghostComponent_verschiebungFun

added theorem WittVector.ghostComponent_zero_verschiebung

added theorem WittVector.ghostComponent_zero_verschiebungFun

added theorem WittVector.map_verschiebung

added def WittVector.verschiebungFun

added theorem WittVector.verschiebungFun_coeff

added theorem WittVector.verschiebungFun_coeff_succ

added theorem WittVector.verschiebungFun_coeff_zero

added def WittVector.verschiebungPoly

added theorem WittVector.verschiebungPoly_zero

added theorem WittVector.verschiebung_coeff_add_one

added theorem WittVector.verschiebung_coeff_succ

added theorem WittVector.verschiebung_coeff_zero

added theorem WittVector.verschiebung_isPoly

Modified Mathlib/RingTheory/WittVector/WittAttributes.lean