Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-20 04:10 ae5b6952

View on Github →

refactor(number_theory/cyclotomic/*): refactor the definition of is_cyclotomic_extension (#14463) We modify the definition of is_cyclotomic_extension, requiring the existence of a primitive root of unity rather than a root of the cyclotomic polynomial. This removes almost all the ne_zero assumptions.

Estimated changes

Modified src/algebra/char_p/basic.lean

added theorem char_p.pow_prime_pow_mul_eq_one_iff

Modified src/algebra/ne_zero.lean

added theorem ne_zero.nat_of_ne_zero

Modified src/number_theory/cyclotomic/basic.lean

modified theorem is_alg_closed.is_cyclotomic_extension

modified theorem is_cyclotomic_extension.adjoin_primitive_root_eq_top

modified theorem is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic

added theorem is_cyclotomic_extension.ne_zero'

added theorem is_cyclotomic_extension.ne_zero

added theorem is_cyclotomic_extension.subsingleton_iff

modified theorem is_cyclotomic_extension.trans

modified theorem is_primitive_root.adjoin_is_cyclotomic_extension

Modified src/number_theory/cyclotomic/discriminant.lean

Modified src/number_theory/cyclotomic/gal.lean

modified theorem is_cyclotomic_extension.from_zeta_aut_spec

Modified src/number_theory/cyclotomic/primitive_roots.lean

added theorem is_cyclotomic_extension.aeval_zeta

modified theorem is_cyclotomic_extension.finrank

modified theorem is_cyclotomic_extension.prime_ne_two_norm_zeta_sub_one

modified theorem is_cyclotomic_extension.prime_ne_two_pow_norm_zeta_pow_sub_one

modified theorem is_cyclotomic_extension.prime_ne_two_pow_norm_zeta_sub_one

modified theorem is_cyclotomic_extension.two_pow_norm_zeta_sub_one

added theorem is_cyclotomic_extension.zeta_is_root

deleted theorem is_cyclotomic_extension.zeta_primitive_root

deleted theorem is_cyclotomic_extension.zeta_spec'

modified theorem is_cyclotomic_extension.zeta_spec

modified theorem is_primitive_root.minpoly_sub_one_eq_cyclotomic_comp

modified theorem is_primitive_root.pow_sub_one_norm_prime_ne_two

modified theorem is_primitive_root.pow_sub_one_norm_prime_pow_ne_two

modified theorem is_primitive_root.pow_sub_one_norm_prime_pow_of_one_le

modified theorem is_primitive_root.pow_sub_one_norm_two

modified theorem is_primitive_root.sub_one_norm_prime

modified theorem is_primitive_root.sub_one_norm_prime_ne_two

modified theorem is_primitive_root.sub_one_norm_two

Modified src/number_theory/cyclotomic/rat.lean

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

modified theorem polynomial.eval_one_cyclotomic_not_prime_pow

Modified src/ring_theory/roots_of_unity.lean

added theorem is_primitive_root.ne_zero'

added theorem mem_roots_of_unity'

added theorem mem_roots_of_unity_prime_pow_mul_iff