Commit 2023-06-08 04:34 dfc4f3db

View on Github →

feat: port RingTheory.WittVector.Basic (#4688)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/Basic.lean

added def WittVector.ghostComponent

added theorem WittVector.ghostComponent_apply

added def WittVector.ghostEquiv

added theorem WittVector.ghostEquiv_coe

added theorem WittVector.ghostMap.bijective_of_invertible

added def WittVector.ghostMap

added theorem WittVector.ghostMap_apply

added theorem WittVector.mapFun.add

added theorem WittVector.mapFun.injective

added theorem WittVector.mapFun.int_cast

added theorem WittVector.mapFun.mul

added theorem WittVector.mapFun.nat_cast

added theorem WittVector.mapFun.neg

added theorem WittVector.mapFun.nsmul

added theorem WittVector.mapFun.one

added theorem WittVector.mapFun.pow

added theorem WittVector.mapFun.sub

added theorem WittVector.mapFun.surjective

added theorem WittVector.mapFun.zero

added theorem WittVector.mapFun.zsmul

added def WittVector.mapFun

added theorem WittVector.map_coeff

added theorem WittVector.map_injective

added theorem WittVector.map_surjective

added theorem WittVector.matrix_vecEmpty_coeff

Modified Mathlib/RingTheory/WittVector/Defs.lean