Theorem IsCyclotomicExtension.discr_prime_pow_ne_two'

Modification history

2025-05-31 11:37

Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

chore(CyclotomicField): use `Nat` instead of `PNat` (#25114) …

Modified IsCyclotomicExtension.discr_prime_pow_ne_two'View on Github →

2023-06-23 04:05

Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

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

Added IsCyclotomicExtension.discr_prime_pow_ne_two'View on Github →