Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-23 09:41 435b97ac

View on Github →

feat(ring_theory/witt_vector): the comparison between W(F_p) and Z_p (#5164) This PR is the culmination of the Witt vector project. We prove that the ring of Witt vectors over zmod p is isomorphic to the ring of p-adic numbers. Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

Modified src/data/equiv/ring.lean

added theorem ring_equiv.symm_to_ring_hom_comp_to_ring_hom

added theorem ring_equiv.to_ring_hom_comp_symm_to_ring_hom

Created src/ring_theory/witt_vector/compare.lean

added theorem truncated_witt_vector.card_zmod

added theorem truncated_witt_vector.char_p_zmod

added theorem truncated_witt_vector.commutes'

added theorem truncated_witt_vector.commutes

added theorem truncated_witt_vector.commutes_symm'

added theorem truncated_witt_vector.commutes_symm

added theorem truncated_witt_vector.eq_of_le_of_cast_pow_eq_zero

added def truncated_witt_vector.zmod_equiv_trunc

added theorem truncated_witt_vector.zmod_equiv_trunc_apply

added def witt_vector.equiv

added def witt_vector.from_padic_int

added theorem witt_vector.from_padic_int_comp_to_padic_int

added theorem witt_vector.from_padic_int_comp_to_padic_int_ext

added def witt_vector.to_padic_int

added theorem witt_vector.to_padic_int_comp_from_padic_int

added theorem witt_vector.to_padic_int_comp_from_padic_int_ext

added def witt_vector.to_zmod_pow

added theorem witt_vector.to_zmod_pow_compat

added theorem witt_vector.zmod_equiv_trunc_compat