Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-04 18:37 5a61ef19

View on Github →

feat(ring_theory/witt_vector/teichmuller): Teichmuller representatives (#4690) Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

Created src/ring_theory/witt_vector/teichmuller.lean

added theorem witt_vector.ghost_component_teichmuller

added theorem witt_vector.map_teichmuller

added theorem witt_vector.teichmuller_coeff_pos

added theorem witt_vector.teichmuller_coeff_zero

added def witt_vector.teichmuller_fun

added theorem witt_vector.teichmuller_zero