Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-01 08:32 30dcd70e

View on Github →

feat(number_theory/cyclotomic/zeta): add lemmas (#11753) Various lemmas about zeta. From flt-regular.

Estimated changes

Modified src/number_theory/cyclotomic/basic.lean

modified theorem is_cyclotomic_extension.finite_dimensional

added theorem is_cyclotomic_extension.is_galois

Modified src/number_theory/cyclotomic/zeta.lean

added theorem is_cyclotomic_extension.finrank

added theorem is_cyclotomic_extension.norm_zeta_eq_one

added theorem is_cyclotomic_extension.norm_zeta_sub_one_eq_eval_cyclotomic

modified def is_cyclotomic_extension.zeta.embeddings_equiv_primitive_roots

modified theorem is_cyclotomic_extension.zeta_minpoly

added theorem is_cyclotomic_extension.zeta_pow

modified theorem is_cyclotomic_extension.zeta_primitive_root