Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-25 16:57 5e8d5274

View on Github →

feat(ring_theory/witt_vector/witt_polynomial): definition and basic properties (#4236) From the Witt vector project This is the first of a dozen of files on Witt vectors. This file contains the definition of the so-called Witt polynomials. Follow-up PRs will contain:

  • An important structural result on the Witt polynomials
  • The definition of the ring of Witt vectors (including the ring structure)
  • Several common operations on Witt vectors
  • Identities between thes operations
  • A comparison isomorphism between the ring of Witt vectors over F_p and the ring of p-adic integers Z_p. Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

added theorem commute_inv_of
deleted def invertible_inv_of
modified theorem mv_polynomial.vars_X
added theorem X_in_terms_of_W_aux
added theorem X_in_terms_of_W_eq
added theorem X_in_terms_of_W_zero
added theorem aeval_witt_polynomial
added theorem map_witt_polynomial
added theorem witt_polynomial_one
added theorem witt_polynomial_vars
added theorem witt_polynomial_zero