mathlib
288802b6 - chore(data/polynomial): slightly generalize `map_eq_zero` and `map_ne_zero` (#4708)

Commit
5 years ago
chore(data/polynomial): slightly generalize `map_eq_zero` and `map_ne_zero` (#4708) We don't need the codomain to be a field.
Author
Parents
Loading