Commit 2023-06-28 10:21 abaae3b8

View on Github →

feat: port RingTheory.WittVector.Truncated (#5538)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/Truncated.lean

added theorem TruncatedWittVector.card

added def TruncatedWittVector.coeff

added theorem TruncatedWittVector.coeff_mk

added theorem TruncatedWittVector.coeff_out

added theorem TruncatedWittVector.coeff_truncate

added theorem TruncatedWittVector.coeff_zero

added theorem TruncatedWittVector.ext

added theorem TruncatedWittVector.ext_iff

added theorem TruncatedWittVector.iInf_ker_truncate

added def TruncatedWittVector.mk

added theorem TruncatedWittVector.mk_coeff

added def TruncatedWittVector.out

added theorem TruncatedWittVector.out_injective

added def TruncatedWittVector.truncate

added theorem TruncatedWittVector.truncateFun_out

added theorem TruncatedWittVector.truncate_comp

added theorem TruncatedWittVector.truncate_comp_wittVector_truncate

added theorem TruncatedWittVector.truncate_surjective

added theorem TruncatedWittVector.truncate_truncate

added theorem TruncatedWittVector.truncate_wittVector_truncate

added def TruncatedWittVector

added theorem WittVector.coeff_truncate

added theorem WittVector.coeff_truncateFun

added theorem WittVector.hom_ext

added def WittVector.lift

added def WittVector.liftEquiv

added def WittVector.liftFun

added theorem WittVector.lift_unique

added theorem WittVector.mem_ker_truncate

added theorem WittVector.out_truncateFun

added def WittVector.truncateFun

added theorem WittVector.truncateFun_add

added theorem WittVector.truncateFun_int_cast

added theorem WittVector.truncateFun_mul

added theorem WittVector.truncateFun_nat_cast

added theorem WittVector.truncateFun_neg

added theorem WittVector.truncateFun_nsmul

added theorem WittVector.truncateFun_one

added theorem WittVector.truncateFun_pow

added theorem WittVector.truncateFun_sub

added theorem WittVector.truncateFun_surjective

added theorem WittVector.truncateFun_zero

added theorem WittVector.truncateFun_zsmul

added theorem WittVector.truncate_comp_lift

added theorem WittVector.truncate_lift

added theorem WittVector.truncate_liftFun

added theorem WittVector.truncate_mk'

added theorem WittVector.truncate_surjective