Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 20:49 93e77412

View on Github →

feat(ring_theory/witt_vector): Witt vectors over a domain are a domain (#11346)

Estimated changes

Modified src/ring_theory/witt_vector/basic.lean

added def witt_vector.constant_coeff

Modified src/ring_theory/witt_vector/defs.lean

added theorem witt_vector.add_coeff_zero

added theorem witt_vector.mul_coeff_zero

Created src/ring_theory/witt_vector/domain.lean

added theorem witt_vector.eq_iterate_verschiebung

added def witt_vector.shift

added theorem witt_vector.shift_coeff

added theorem witt_vector.verschiebung_nonzero

added theorem witt_vector.verschiebung_shift

Modified src/ring_theory/witt_vector/identities.lean

added theorem witt_vector.coeff_p_pow_eq_zero

added theorem witt_vector.iterate_frobenius_coeff

added theorem witt_vector.iterate_verschiebung_coeff

added theorem witt_vector.iterate_verschiebung_mul

added theorem witt_vector.iterate_verschiebung_mul_coeff

added theorem witt_vector.iterate_verschiebung_mul_left

added theorem witt_vector.mul_char_p_coeff_succ

added theorem witt_vector.mul_char_p_coeff_zero

added theorem witt_vector.verschiebung_frobenius

added theorem witt_vector.verschiebung_frobenius_comm