Commit 2023-06-28 18:09 f90c0b29

View on Github →

feat: port ring theory.witt_vector.compare (#5555)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/Compare.lean

added theorem TruncatedWittVector.card_zMod

added theorem TruncatedWittVector.charP_zMod

added theorem TruncatedWittVector.commutes'

added theorem TruncatedWittVector.commutes

added theorem TruncatedWittVector.commutes_symm'

added theorem TruncatedWittVector.commutes_symm

added theorem TruncatedWittVector.eq_of_le_of_cast_pow_eq_zero

added def TruncatedWittVector.zmodEquivTrunc

added theorem TruncatedWittVector.zmodEquivTrunc_apply

added def WittVector.equiv

added def WittVector.fromPadicInt

added theorem WittVector.fromPadicInt_comp_toPadicInt

added theorem WittVector.fromPadicInt_comp_toPadicInt_ext

added def WittVector.toPadicInt

added theorem WittVector.toPadicInt_comp_fromPadicInt

added theorem WittVector.toPadicInt_comp_fromPadicInt_ext

added def WittVector.toZmodPow

added theorem WittVector.toZmodPow_compat

added theorem WittVector.zmodEquivTrunc_compat