Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-13 06:36 14790682

View on Github →

chore(ring_theory/polynomial/cyclotomic): fix namespacing (#9116) @riccardobrasca told me I got it wrong, so I fixed it :)

Estimated changes

Modified src/number_theory/primes_congruent_one.lean

Modified src/ring_theory/polynomial/cyclotomic.lean

added theorem minpoly_dvd_cyclotomic

deleted theorem polynomial.minpoly_primitive_root_dvd_cyclotomic

deleted theorem polynomial.order_of_root_cyclotomic

added theorem polynomial.order_of_root_cyclotomic_eq