mathlib
342a4b0a - feat(data/polynomial/coeff): add `char_zero` instance on polynomials (#13075)

Commit
3 years ago
feat(data/polynomial/coeff): add `char_zero` instance on polynomials (#13075) Besides adding the instance, I also added a warning on the difference between `char_zero R` and `char_p R 0` for general semirings. An example showing the difference is in #13080. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F)
Author
Parents
Loading