Mathlib v3 is deprecated. Go to Mathlib v4

Theorem witt_vector.sub_eq

Modification history

2020-12-19 14:59
src/ring_theory/witt_vector/is_poly.lean
feat(ring_theory/witt_vector): redefine subtraction using witt_sub polynomial (#5405)
Deleted witt_vector.sub_eqView on Github →
2020-12-03 12:03
src/ring_theory/witt_vector/is_poly.lean
feat(ring_theory/witt_vector): witt_sub, a demonstration of is_poly techniques (#5165) …
Added witt_vector.sub_eqView on Github →