Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-17 00:33 a2630fc3

View on Github →

chore(field_theory|ring_theory|linear_algebra): rename minimal_polynomial to minpoly (#5771) This PR renames:

  • minimal_polynomial -> minpoly
  • a similar substitution throughout the library for all names containing the substring minimal_polynomial
  • fixed_points.minpoly.minimal_polynomial -> fixed_points.minpoly_eq_minpoly This PR moves a file: src/field_theory/minimal_polynomial.lean -> src/field_theory/minpoly.lean

Estimated changes

deleted theorem minimal_polynomial.aeval
deleted theorem minimal_polynomial.dvd
deleted theorem minimal_polynomial.min
deleted theorem minimal_polynomial.monic
deleted theorem minimal_polynomial.one
deleted theorem minimal_polynomial.prime
deleted theorem minimal_polynomial.root
deleted theorem minimal_polynomial.unique
deleted theorem minimal_polynomial.zero
added theorem minpoly.aeval
added theorem minpoly.degree_pos
added theorem minpoly.dvd
added theorem minpoly.eq_X_sub_C
added theorem minpoly.gcd_domain_dvd
added theorem minpoly.integer_dvd
added theorem minpoly.irreducible
added theorem minpoly.min
added theorem minpoly.monic
added theorem minpoly.ne_zero
added theorem minpoly.not_is_unit
added theorem minpoly.one
added theorem minpoly.prime
added theorem minpoly.root
added theorem minpoly.unique'
added theorem minpoly.unique
added theorem minpoly.zero