Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-16 13:55 1b010684

View on Github →

feat(ring_theory/witt_vector): Witt vectors are proj. limit of truncated Witt vectors (#5163) Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

Modified src/ring_theory/witt_vector/truncated.lean

added theorem truncated_witt_vector.card

added theorem truncated_witt_vector.coeff_truncate

added theorem truncated_witt_vector.infi_ker_truncate

added def truncated_witt_vector.truncate

added theorem truncated_witt_vector.truncate_comp

added theorem truncated_witt_vector.truncate_comp_witt_vector_truncate

added theorem truncated_witt_vector.truncate_surjective

added theorem truncated_witt_vector.truncate_truncate

added theorem truncated_witt_vector.truncate_witt_vector_truncate

added theorem witt_vector.coeff_truncate

added theorem witt_vector.hom_ext

added def witt_vector.lift

added def witt_vector.lift_equiv

added def witt_vector.lift_fun

added theorem witt_vector.lift_unique

added theorem witt_vector.mem_ker_truncate

added def witt_vector.truncate

added theorem witt_vector.truncate_comp_lift

added theorem witt_vector.truncate_lift

added theorem witt_vector.truncate_lift_fun

added theorem witt_vector.truncate_mk

added theorem witt_vector.truncate_surjective