Commit 2023-06-07 15:05 52f16527

View on Github →

feat: port RingTheory.Polynomial.Cyclotomic.Basic (#4805)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

added theorem Polynomial.X_pow_sub_one_dvd_prod_cyclotomic

added theorem Polynomial.X_pow_sub_one_eq_prod

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.X_pow_sub_one_splits

added theorem Polynomial.coprime_of_root_cyclotomic

added theorem Polynomial.cyclotomic'.monic

added def Polynomial.cyclotomic'

added theorem Polynomial.cyclotomic'_eq_X_pow_sub_one_div

added theorem Polynomial.cyclotomic'_ne_zero

added theorem Polynomial.cyclotomic'_one

added theorem Polynomial.cyclotomic'_splits

added theorem Polynomial.cyclotomic'_two

added theorem Polynomial.cyclotomic'_zero

added theorem Polynomial.cyclotomic.dvd_X_pow_sub_one

added theorem Polynomial.cyclotomic.eval_apply

added theorem Polynomial.cyclotomic.isPrimitive

added theorem Polynomial.cyclotomic.monic

added def Polynomial.cyclotomic

added theorem Polynomial.cyclotomic_coeff_zero

added theorem Polynomial.cyclotomic_dvd_geom_sum_of_dvd

added theorem Polynomial.cyclotomic_eq_X_pow_sub_one_div

added theorem Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius

added theorem Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots

added theorem Polynomial.cyclotomic_ne_zero

added theorem Polynomial.cyclotomic_one

added theorem Polynomial.cyclotomic_prime

added theorem Polynomial.cyclotomic_prime_mul_X_sub_one

added theorem Polynomial.cyclotomic_prime_pow_eq_geom_sum

added theorem Polynomial.cyclotomic_prime_pow_mul_X_pow_sub_one

added theorem Polynomial.cyclotomic_three

added theorem Polynomial.cyclotomic_two

added theorem Polynomial.cyclotomic_zero

added theorem Polynomial.degree_cyclotomic'

added theorem Polynomial.degree_cyclotomic

added theorem Polynomial.degree_cyclotomic_pos

added theorem Polynomial.eq_cyclotomic_iff

added theorem Polynomial.int_coeff_of_cyclotomic'

added theorem Polynomial.int_cyclotomic_rw

added theorem Polynomial.int_cyclotomic_spec

added theorem Polynomial.int_cyclotomic_unique

added theorem Polynomial.map_cyclotomic

added theorem Polynomial.map_cyclotomic_int

added theorem Polynomial.natDegree_cyclotomic'

added theorem Polynomial.natDegree_cyclotomic

added theorem Polynomial.orderOf_root_cyclotomic_dvd

added theorem Polynomial.prod_cyclotomic'_eq_X_pow_sub_one

added theorem Polynomial.prod_cyclotomic_eq_X_pow_sub_one

added theorem Polynomial.prod_cyclotomic_eq_geom_sum

added theorem Polynomial.roots_of_cyclotomic

added theorem Polynomial.unique_int_coeff_of_cycl