Commit 2023-05-24 14:35 5bfbcca0

View on Github →

chore(ring_theory.polynomial.cyclotomic): split file (#19077) ring_theory.polynomial.cyclotomic is almost 1000 lines long and it can be nicely split. We also fix some docstring.

Estimated changes

Modified archive/100-theorems-list/37_solution_of_cubic.lean

Modified src/number_theory/cyclotomic/basic.lean

Modified src/number_theory/cyclotomic/primitive_roots.lean

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

deleted theorem is_primitive_root.is_root_cyclotomic

deleted theorem is_primitive_root.minpoly_dvd_cyclotomic

deleted theorem is_primitive_root.minpoly_eq_cyclotomic_of_irreducible

deleted theorem is_root_of_unity_iff

deleted theorem polynomial.cyclotomic.irreducible

deleted theorem polynomial.cyclotomic.irreducible_rat

deleted theorem polynomial.cyclotomic.is_coprime_rat

deleted theorem polynomial.cyclotomic.roots_eq_primitive_roots_val

deleted theorem polynomial.cyclotomic.roots_to_finset_eq_primitive_roots

deleted theorem polynomial.cyclotomic_eq_minpoly

deleted theorem polynomial.cyclotomic_eq_minpoly_rat

deleted theorem polynomial.cyclotomic_expand_eq_cyclotomic

deleted theorem polynomial.cyclotomic_expand_eq_cyclotomic_mul

deleted theorem polynomial.cyclotomic_injective

deleted theorem polynomial.cyclotomic_irreducible_of_irreducible_pow

deleted theorem polynomial.cyclotomic_irreducible_pow_of_irreducible_pow

deleted theorem polynomial.cyclotomic_mul_prime_dvd_eq_pow

deleted theorem polynomial.cyclotomic_mul_prime_eq_pow_of_not_dvd

deleted theorem polynomial.cyclotomic_mul_prime_pow_eq

deleted theorem polynomial.is_root_cyclotomic_iff

deleted theorem polynomial.is_root_cyclotomic_iff_char_zero

deleted theorem polynomial.is_root_cyclotomic_prime_pow_mul_iff_of_char_p

deleted theorem polynomial.is_root_of_unity_of_root_cyclotomic

deleted theorem polynomial.roots_cyclotomic_nodup

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

Created src/ring_theory/polynomial/cyclotomic/expand.lean

added theorem polynomial.cyclotomic_expand_eq_cyclotomic

added theorem polynomial.cyclotomic_expand_eq_cyclotomic_mul

added theorem polynomial.cyclotomic_irreducible_of_irreducible_pow

added theorem polynomial.cyclotomic_irreducible_pow_of_irreducible_pow

added theorem polynomial.cyclotomic_mul_prime_dvd_eq_pow

added theorem polynomial.cyclotomic_mul_prime_eq_pow_of_not_dvd

added theorem polynomial.cyclotomic_mul_prime_pow_eq

added theorem polynomial.is_root_cyclotomic_prime_pow_mul_iff_of_char_p

Created src/ring_theory/polynomial/cyclotomic/roots.lean

added theorem is_primitive_root.is_root_cyclotomic

added theorem is_primitive_root.minpoly_dvd_cyclotomic

added theorem is_primitive_root.minpoly_eq_cyclotomic_of_irreducible

added theorem is_root_of_unity_iff

added theorem polynomial.cyclotomic.irreducible

added theorem polynomial.cyclotomic.irreducible_rat

added theorem polynomial.cyclotomic.is_coprime_rat

added theorem polynomial.cyclotomic.roots_eq_primitive_roots_val

added theorem polynomial.cyclotomic.roots_to_finset_eq_primitive_roots

added theorem polynomial.cyclotomic_eq_minpoly

added theorem polynomial.cyclotomic_eq_minpoly_rat

added theorem polynomial.cyclotomic_injective

added theorem polynomial.is_root_cyclotomic_iff

added theorem polynomial.is_root_cyclotomic_iff_char_zero

added theorem polynomial.is_root_of_unity_of_root_cyclotomic

added theorem polynomial.roots_cyclotomic_nodup

Modified src/ring_theory/polynomial/eisenstein/is_integral.lean