Theorems · Theorem · number theory
IsCyclotomicExtension.Rat.discr_prime
∀ (p : ℕ) (K : Type u) [inst : Field K] [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
[inst_2 : IsCyclotomicExtension {p} ℚ K], NumberField.discr K = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)We compute the absolute discriminant of a p-th cyclotomic field where p is prime.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 229 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Fieldstatement and proof · cited by 7,404
- Set.Elemstatement · cited by 7,166
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- Factstatement and proof · cited by 2,726
- zero_addproof · cited by 2,366
- Nat.Primestatement and proof · cited by 2,059
- pow_zeroproof · cited by 1,094
- CharZerostatement and proof · cited by 932
- pow_oneproof · cited by 894
- IsCyclotomicExtensionstatement and proof · cited by 220
Cited by2
Results whose statement or proof uses this declaration.
- IsCyclotomicExtension.Rat.five_pidproof · cited by 0
- IsCyclotomicExtension.Rat.three_pidproof · cited by 0