Theorem IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow

Modification history

2023-06-23 04:05
Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
feat: port NumberTheory.Cyclotomic.Discriminant (#5413)
Added IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_powView on Github →