Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-15 12:59 5bcffd96

View on Github →

feat(number_theory/cyclotomic/zeta): add lemmas (#11786) Lemmas about the norm of ζ - 1. From flt-regular.

depends on: #11941

Estimated changes

Modified src/number_theory/cyclotomic/primitive_roots.lean

added theorem is_cyclotomic_extension.is_prime_pow.norm_zeta_sub_one

added theorem is_cyclotomic_extension.norm_zeta_eq_one

added theorem is_cyclotomic_extension.prime_ne_two.norm_zeta_sub_one

added theorem is_cyclotomic_extension.prime_ne_two_pow.norm_zeta_sub_one

added theorem is_cyclotomic_extension.two_pow.norm_zeta_sub_one

added theorem is_primitive_root.prime_ne_two_pow.sub_one_norm

added theorem is_primitive_root.sub_one_norm.is_prime_pow

added theorem is_primitive_root.sub_one_norm.pow_two

added theorem is_primitive_root.sub_one_norm.prime

modified theorem is_primitive_root.sub_one_norm_eq_eval_cyclotomic