Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-09 21:43 09a505a7

View on Github →

feat(ring_theory/witt_vector): use structure instead of irreducible (#6604)

Estimated changes

Modified src/data/matrix/notation.lean

added theorem matrix.cons_fin_one

Modified src/ring_theory/witt_vector/basic.lean

modified def witt_vector.map_fun

added theorem witt_vector.matrix_vec_empty_coeff

Modified src/ring_theory/witt_vector/defs.lean

deleted def witt_vector.coeff

modified theorem witt_vector.coeff_mk

deleted def witt_vector.mk

added theorem witt_vector.v2_coeff

added structure witt_vector

deleted def witt_vector

Modified src/ring_theory/witt_vector/frobenius.lean

Modified src/ring_theory/witt_vector/init_tail.lean

Modified src/ring_theory/witt_vector/is_poly.lean

Modified src/ring_theory/witt_vector/teichmuller.lean

modified def witt_vector.teichmuller_fun

Modified src/ring_theory/witt_vector/truncated.lean

Modified src/ring_theory/witt_vector/verschiebung.lean