Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-04 00:19 d3e8e0a0

View on Github →

chore(field_theory/minpoly): Split results from minpoly.lean into three files (#18048) In this PR, we split the results contained in minpoly.lean into three separate files: minpoly.basic.lean, minpoly.field.lean and minpoly.gcd_monoid.lean. This is helpful for PR #18021.

Estimated changes

deleted theorem minpoly.add_algebra_map
deleted theorem minpoly.aeval
deleted theorem minpoly.degree_pos
deleted theorem minpoly.dvd
deleted theorem minpoly.eq_X_sub_C'
deleted theorem minpoly.eq_X_sub_C
deleted theorem minpoly.eq_of_irreducible
deleted theorem minpoly.eq_zero
deleted theorem minpoly.gcd_domain_dvd
deleted theorem minpoly.gcd_domain_unique
deleted theorem minpoly.irreducible
deleted theorem minpoly.map_ne_one
deleted theorem minpoly.min
deleted theorem minpoly.monic
deleted theorem minpoly.nat_degree_pos
deleted theorem minpoly.ne_one
deleted theorem minpoly.ne_zero
deleted theorem minpoly.not_is_unit
deleted theorem minpoly.one
deleted theorem minpoly.prime
deleted theorem minpoly.root
deleted theorem minpoly.sub_algebra_map
deleted theorem minpoly.subsingleton
deleted theorem minpoly.unique
deleted theorem minpoly.zero
added theorem minpoly.aeval
added theorem minpoly.degree_pos
added theorem minpoly.eq_zero
added theorem minpoly.irreducible
added theorem minpoly.map_ne_one
added theorem minpoly.min
added theorem minpoly.monic
added theorem minpoly.nat_degree_pos
added theorem minpoly.ne_one
added theorem minpoly.ne_zero
added theorem minpoly.not_is_unit
added theorem minpoly.subsingleton
added theorem minpoly.dvd
added theorem minpoly.eq_X_sub_C'
added theorem minpoly.eq_X_sub_C
added theorem minpoly.one
added theorem minpoly.prime
added theorem minpoly.root
added theorem minpoly.unique
added theorem minpoly.zero
added theorem minpoly.gcd_domain_dvd