Commit 2023-06-15 11:52 5f9c1678

View on Github →

chore: forward-port leanprover-community/mathlib#19182 (#5024) The important thing to forward-port here is the addition of [DecidableEq _] to a handful of lemmas. linear_algebra.eigenspace.minpoly did not need anything forward-porting, as the proof which broke in mathlib3 did not break in mathlib4. The nthRootsFinset_def lemma was forgotten in the mathlib3 PR.

Estimated changes

Modified Mathlib/Data/Polynomial/RingDivision.lean

modified theorem Polynomial.bUnion_roots_finite

modified theorem Polynomial.card_nthRoots

modified theorem Polynomial.count_map_roots

modified theorem Polynomial.count_map_roots_of_injective

modified theorem Polynomial.count_roots

modified theorem Polynomial.degree_le_mul_left

modified theorem Polynomial.exists_multiset_roots

modified theorem Polynomial.map_roots_le

modified theorem Polynomial.mem_nthRootsFinset

modified theorem Polynomial.natDegree_pow

added theorem Polynomial.nthRootsFinset_def

modified theorem Polynomial.nthRootsFinset_zero

modified theorem Polynomial.prod_multiset_root_eq_finset_root

modified theorem Polynomial.rootMultiplicity_X_sub_C

modified theorem Polynomial.rootSet_def

modified theorem Polynomial.roots_C

added theorem Polynomial.roots_def

modified theorem Polynomial.roots_mul

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean