Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-14 23:13 65442444

View on Github →

feat(data/polynomial) small refactor and golf (#5002) Factor out the lemma that roots of the normalization equal the roots of a polynomial and golf a proof a tiny bit.

Estimated changes