Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-03 21:32 1af53ff5

View on Github →

feat(polynomial/cyclotomic): some divisibility results (#12426)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.not_mem_sdiff_of_not_mem_left

Modified src/data/polynomial/eval.lean

added theorem polynomial.map_dvd

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

added theorem polynomial.X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd

added theorem polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd

added theorem polynomial.cyclotomic_dvd_geom_sum_of_dvd