Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-03 17:56 e88a5bb5

View on Github →

feat(*): assorted prereqs for cyclotomic polynomials (#4887) This is hopefully my last preparatory PR for cyclotomic polynomials. It was in 4869 .

Estimated changes

Modified src/data/polynomial/ring_division.lean

modified theorem polynomial.mem_nth_roots_finset

modified def polynomial.nth_roots_finset

Modified src/number_theory/divisors.lean

modified theorem nat.filter_dvd_eq_divisors

Modified src/ring_theory/roots_of_unity.lean

modified theorem is_primitive_root.card_nth_roots

modified theorem is_primitive_root.card_nth_roots_finset

modified theorem is_primitive_root.nth_roots_nodup

added theorem is_primitive_root.nth_roots_one_eq_bind_primitive_roots'

modified theorem is_primitive_root.nth_roots_one_eq_bind_primitive_roots

added theorem is_primitive_root.primitive_root_one

added theorem is_primitive_root.primitive_roots_zero