Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-19 15:34 47542a04

View on Github →

feat(ring_theory/witt_vector/verschiebung): verschiebung of witt vectors (#4836) Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

Created src/ring_theory/witt_vector/verschiebung.lean

added theorem witt_vector.aeval_verschiebung_poly'

added theorem witt_vector.aeval_verschiebung_poly

added theorem witt_vector.bind₁_verschiebung_poly_witt_polynomial

added theorem witt_vector.ghost_component_verschiebung

added theorem witt_vector.ghost_component_verschiebung_fun

added theorem witt_vector.ghost_component_zero_verschiebung

added theorem witt_vector.ghost_component_zero_verschiebung_fun

added theorem witt_vector.map_verschiebung

added def witt_vector.verschiebung

added theorem witt_vector.verschiebung_coeff_add_one

added theorem witt_vector.verschiebung_coeff_succ

added theorem witt_vector.verschiebung_coeff_zero

added def witt_vector.verschiebung_fun

added theorem witt_vector.verschiebung_fun_coeff

added theorem witt_vector.verschiebung_fun_coeff_succ

added theorem witt_vector.verschiebung_fun_coeff_zero

added theorem witt_vector.verschiebung_fun_is_poly

added theorem witt_vector.verschiebung_is_poly

added def witt_vector.verschiebung_poly

added theorem witt_vector.verschiebung_poly_zero