Commit 2023-06-22 16:17 b89833e5

View on Github →

feat: port NumberTheory.Cyclotomic.PrimitiveRoots (#5384)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

added theorem IsCyclotomicExtension.aeval_zeta

added theorem IsCyclotomicExtension.finrank

added theorem IsCyclotomicExtension.isPrimePow_norm_zeta_sub_one

added theorem IsCyclotomicExtension.norm_zeta_eq_one

added theorem IsCyclotomicExtension.prime_ne_two_norm_zeta_sub_one

added theorem IsCyclotomicExtension.prime_ne_two_pow_norm_zeta_pow_sub_one

added theorem IsCyclotomicExtension.prime_ne_two_pow_norm_zeta_sub_one

added theorem IsCyclotomicExtension.two_pow_norm_zeta_sub_one

added theorem IsCyclotomicExtension.zeta_isRoot

added theorem IsCyclotomicExtension.zeta_pow

added theorem IsCyclotomicExtension.zeta_spec

added theorem IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe

added theorem IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp

added theorem IsPrimitiveRoot.norm_eq_neg_one_pow

added theorem IsPrimitiveRoot.norm_eq_one

added theorem IsPrimitiveRoot.norm_eq_one_of_linearly_ordered

added theorem IsPrimitiveRoot.norm_of_cyclotomic_irreducible

added theorem IsPrimitiveRoot.pow_sub_one_norm_prime_ne_two

added theorem IsPrimitiveRoot.pow_sub_one_norm_prime_pow_ne_two

added theorem IsPrimitiveRoot.pow_sub_one_norm_prime_pow_of_ne_zero

added theorem IsPrimitiveRoot.pow_sub_one_norm_two

added theorem IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one

added theorem IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic

added theorem IsPrimitiveRoot.sub_one_norm_isPrimePow

added theorem IsPrimitiveRoot.sub_one_norm_prime

added theorem IsPrimitiveRoot.sub_one_norm_prime_ne_two

added theorem IsPrimitiveRoot.sub_one_norm_two