Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-14 21:04 0a6c26ee

View on Github →

feat(ring_theory/power_basis): minpoly_gen is always the minimal polynomial (#18117)

  • add minpoly.unique', a characterization for being the minimal polynomial.
  • golf various proofs and remove some unnecessary typeclass assumptions.

Estimated changes

modified theorem minpoly.degree_pos
modified theorem minpoly.nat_degree_pos
added theorem minpoly.unique'
added theorem linear_independent_pow
modified theorem power_basis.minpoly_gen_eq