Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-17 18:30 579ec7d3

View on Github →

feat(ring_theory/power_basis): pb.minpoly_gen = minpoly pb.gen (#8719) It actually kind of surprised me that this lemma was never added!

Estimated changes