Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-13 07:07 8efcf802

View on Github →

refactor(data/polynomial/ring_division): remove open_locale classical (#19182) This makes the lemmas strictly more general.

Estimated changes

Modified src/data/polynomial/ring_division.lean

modified theorem polynomial.bUnion_roots_finite

modified theorem polynomial.count_map_roots

modified theorem polynomial.count_map_roots_of_injective

modified theorem polynomial.count_roots

modified theorem polynomial.exists_multiset_roots

modified theorem polynomial.prod_multiset_root_eq_finset_root

modified theorem polynomial.root_multiplicity_X_sub_C

modified theorem polynomial.root_set_def

added theorem polynomial.roots_def

Modified src/linear_algebra/eigenspace/minpoly.lean