Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-26 13:22 2e90c600

View on Github →

feat(ring_theory/witt_vector/basic): verifying the ring axioms (#4694) Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

Created src/ring_theory/witt_vector/basic.lean

added def witt_vector.ghost_component

added theorem witt_vector.ghost_component_apply

added def witt_vector.ghost_equiv

added theorem witt_vector.ghost_equiv_coe

added theorem witt_vector.ghost_map.bijective_of_invertible

added def witt_vector.ghost_map

added theorem witt_vector.ghost_map_apply

added def witt_vector.map

added theorem witt_vector.map_coeff

added theorem witt_vector.map_fun.add

added theorem witt_vector.map_fun.injective

added theorem witt_vector.map_fun.mul

added theorem witt_vector.map_fun.neg

added theorem witt_vector.map_fun.one

added theorem witt_vector.map_fun.surjective

added theorem witt_vector.map_fun.zero

added def witt_vector.map_fun

added theorem witt_vector.map_injective

added theorem witt_vector.map_surjective