Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-20 05:38 288802b6

View on Github →

chore(data/polynomial): slightly generalize map_eq_zero and map_ne_zero (#4708) We don't need the codomain to be a field.

Estimated changes

Modified src/data/polynomial/field_division.lean

modified theorem polynomial.map_eq_zero

modified theorem polynomial.map_ne_zero