Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-11 12:35 d2ae4e25

View on Github →

feat(ring_theory/witt_vector): truncated Witt vectors, definition and ring structure (#5162) Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

Created src/ring_theory/witt_vector/truncated.lean

added def truncated_witt_vector.coeff

added theorem truncated_witt_vector.coeff_mk

added theorem truncated_witt_vector.coeff_out

added theorem truncated_witt_vector.coeff_zero

added theorem truncated_witt_vector.ext

added theorem truncated_witt_vector.ext_iff

added def truncated_witt_vector.mk

added theorem truncated_witt_vector.mk_coeff

added def truncated_witt_vector.out

added theorem truncated_witt_vector.out_injective

added theorem truncated_witt_vector.truncate_fun_out

added def truncated_witt_vector

added theorem witt_vector.coeff_truncate_fun

added theorem witt_vector.out_truncate_fun

added def witt_vector.truncate_fun

added theorem witt_vector.truncate_fun_add

added theorem witt_vector.truncate_fun_mul

added theorem witt_vector.truncate_fun_neg

added theorem witt_vector.truncate_fun_one

added theorem witt_vector.truncate_fun_surjective

added theorem witt_vector.truncate_fun_zero