Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-22 06:16 bef50a4d

View on Github →

feat(field_theory/minpoly): Minimal polynomials of degree one (#5844) If the minimal polynomial has degree one then the element in question lies in the base ring.

Estimated changes