Commit 2023-06-23 04:05 6985e17b

View on Github →

feat: port NumberTheory.Cyclotomic.Discriminant (#5413)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

added theorem IsCyclotomicExtension.discr_odd_prime

added theorem IsCyclotomicExtension.discr_prime_pow

added theorem IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow

added theorem IsCyclotomicExtension.discr_prime_pow_ne_two'

added theorem IsCyclotomicExtension.discr_prime_pow_ne_two

added theorem IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one