Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-27 16:04 8ef4331c

View on Github →

feat(ring_theory/witt_vector): Witt vectors are a DVR (#12213) This PR adds two connected files. mul_coeff.lean adds an auxiliary result that's used in a few places in #12041 . One of these places is in discrete_valuation_ring.lean, which shows that Witt vectors over a perfect field form a DVR.

Estimated changes

Created src/ring_theory/witt_vector/discrete_valuation_ring.lean

added theorem witt_vector.coe_mk_unit

added theorem witt_vector.exists_eq_pow_p_mul'

added theorem witt_vector.exists_eq_pow_p_mul

added theorem witt_vector.irreducible

added theorem witt_vector.is_unit_of_coeff_zero_ne_zero

added def witt_vector.mk_unit

added def witt_vector.succ_nth_val_units

Modified src/ring_theory/witt_vector/identities.lean

added theorem witt_vector.coeff_p

added theorem witt_vector.coeff_p_one

added theorem witt_vector.coeff_p_zero

Created src/ring_theory/witt_vector/mul_coeff.lean

added theorem witt_vector.mul_poly_of_interest_aux1

added theorem witt_vector.mul_poly_of_interest_aux2

added theorem witt_vector.mul_poly_of_interest_aux3

added theorem witt_vector.mul_poly_of_interest_aux4

added theorem witt_vector.mul_poly_of_interest_aux5

added theorem witt_vector.mul_poly_of_interest_vars

added theorem witt_vector.nth_mul_coeff'

added theorem witt_vector.nth_mul_coeff

added def witt_vector.nth_remainder

added theorem witt_vector.nth_remainder_spec

added theorem witt_vector.peval_poly_of_interest'

added theorem witt_vector.peval_poly_of_interest

added def witt_vector.poly_of_interest

added theorem witt_vector.poly_of_interest_vars

added theorem witt_vector.poly_of_interest_vars_eq

added def witt_vector.remainder

added theorem witt_vector.remainder_vars

added def witt_vector.witt_poly_prod

added def witt_vector.witt_poly_prod_remainder

added theorem witt_vector.witt_poly_prod_remainder_vars

added theorem witt_vector.witt_poly_prod_vars