Mathlib Changelog
v4
Changelog
About
Github
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