Documentation

Mathlib.NumberTheory.Cyclotomic.Rat

Ring of integers of p ^ n-th cyclotomic fields #

We gather results about cyclotomic extensions of . In particular, we compute the ring of integers of a p ^ n-th cyclotomic extension of .

Main results #

theorem IsCyclotomicExtension.Rat.discr_prime_pow_ne_two' {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hk : p ^ (k + 1) 2) :
Algebra.discr (IsPrimitiveRoot.subOnePowerBasis ).basis = (-1) ^ ((p ^ (k + 1)).totient / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

The discriminant of the power basis given by ζ - 1.

theorem IsCyclotomicExtension.Rat.discr_odd_prime' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) (hodd : p 2) :
Algebra.discr (IsPrimitiveRoot.subOnePowerBasis ).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)
theorem IsCyclotomicExtension.Rat.discr_prime_pow' {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
Algebra.discr (IsPrimitiveRoot.subOnePowerBasis ).basis = (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

The discriminant of the power basis given by ζ - 1. Beware that in the cases p ^ k = 1 and p ^ k = 2 the formula uses 1 / 2 = 0 and 0 - 1 = 0. It is useful only to have a uniform result. See also IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'.

theorem IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow' {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
∃ (u : ˣ) (n : ), Algebra.discr (IsPrimitiveRoot.subOnePowerBasis ).basis = u * p ^ n

If p is a prime and IsCyclotomicExtension {p ^ k} K L, then there are u : ℤˣ and n : ℕ such that the discriminant of the power basis given by ζ - 1 is u * p ^ n. Often this is enough and less cumbersome to use than IsCyclotomicExtension.Rat.discr_prime_pow'.

theorem IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :

If K is a p ^ k-th cyclotomic extension of , then (adjoin ℤ {ζ}) is the integral closure of in K.

The integral closure of inside CyclotomicField (p ^ k) ℚ is CyclotomicRing (p ^ k) ℤ ℚ.

@[simp]
theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) (a : NumberField.RingOfIntegers K) :
.adjoinEquivRingOfIntegers.symm a = (IsIntegralClosure.lift ((Algebra.adjoin {ζ})) K) a
@[simp]
theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) (a : (Algebra.adjoin {ζ})) :
.adjoinEquivRingOfIntegers a = (IsIntegralClosure.lift (NumberField.RingOfIntegers K) K) a
noncomputable def IsPrimitiveRoot.adjoinEquivRingOfIntegers {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :

The algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive p ^ k-th root of unity and K is a p ^ k-th cyclotomic extension of .

Equations
Instances For

    The ring of integers of a p ^ k-th cyclotomic extension of is a cyclotomic extension.

    Equations
    • =
    noncomputable def IsPrimitiveRoot.integralPowerBasis {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :

    The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a p ^ k cyclotomic extension of .

    Equations
    Instances For
      @[reducible, inline]
      abbrev IsPrimitiveRoot.toInteger {K : Type u} [Field K] {ζ : K} {k : ℕ+} (hζ : IsPrimitiveRoot ζ k) :

      Abbreviation to see a primitive root of unity as a member of the ring of integers.

      Equations
      • .toInteger = ζ,
      Instances For
        theorem IsPrimitiveRoot.coe_toInteger {K : Type u} [Field K] {ζ : K} {k : ℕ+} (hζ : IsPrimitiveRoot ζ k) :
        .toInteger = ζ
        theorem IsPrimitiveRoot.finite_quotient_toInteger_sub_one {K : Type u} [Field K] {ζ : K} [NumberField K] {k : ℕ+} (hk : 1 < k) (hζ : IsPrimitiveRoot ζ k) :

        𝓞 K ⧸ Ideal.span {ζ - 1} is finite.

        theorem IsPrimitiveRoot.card_quotient_toInteger_sub_one {K : Type u} [Field K] {ζ : K} [NumberField K] {k : ℕ+} (hk : 1 < k) (hζ : IsPrimitiveRoot ζ k) :
        Nat.card (NumberField.RingOfIntegers K Ideal.span {.toInteger - 1}) = ((Algebra.norm ) (.toInteger - 1)).natAbs

        We have that 𝓞 K ⧸ Ideal.span {ζ - 1} has cardinality equal to the norm of ζ - 1.

        See the results below to compute this norm in various cases.

        theorem IsPrimitiveRoot.toInteger_isPrimitiveRoot {K : Type u} [Field K] {ζ : K} {k : ℕ+} (hζ : IsPrimitiveRoot ζ k) :
        IsPrimitiveRoot .toInteger k
        @[simp]
        theorem IsPrimitiveRoot.integralPowerBasis_gen {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
        .integralPowerBasis.gen = .toInteger
        @[simp]
        theorem IsPrimitiveRoot.integralPowerBasis_dim {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
        .integralPowerBasis.dim = (p ^ k).totient
        @[simp]
        theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers'_apply {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) (a : (Algebra.adjoin {ζ})) :
        .adjoinEquivRingOfIntegers' a = (IsIntegralClosure.lift (NumberField.RingOfIntegers K) K) a
        @[simp]
        theorem IsPrimitiveRoot.adjoinEquivRingOfIntegers'_symm_apply {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) (a : NumberField.RingOfIntegers K) :
        .adjoinEquivRingOfIntegers'.symm a = (IsIntegralClosure.lift ((Algebra.adjoin {ζ})) K) a
        noncomputable def IsPrimitiveRoot.adjoinEquivRingOfIntegers' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) :

        The algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive p-th root of unity and K is a p-th cyclotomic extension of .

        Equations
        • .adjoinEquivRingOfIntegers' = .adjoinEquivRingOfIntegers
        Instances For

          The ring of integers of a p-th cyclotomic extension of is a cyclotomic extension.

          Equations
          • =
          noncomputable def IsPrimitiveRoot.integralPowerBasis' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) :

          The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a p-th cyclotomic extension of .

          Equations
          • .integralPowerBasis' = .integralPowerBasis
          Instances For
            @[simp]
            theorem IsPrimitiveRoot.integralPowerBasis'_gen {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) :
            .integralPowerBasis'.gen = .toInteger
            @[simp]
            theorem IsPrimitiveRoot.power_basis_int'_dim {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) :
            .integralPowerBasis'.dim = (p).totient
            noncomputable def IsPrimitiveRoot.subOneIntegralPowerBasis {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :

            The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a p ^ k cyclotomic extension of .

            Equations
            • .subOneIntegralPowerBasis = .integralPowerBasis.ofGenMemAdjoin'
            Instances For
              @[simp]
              theorem IsPrimitiveRoot.subOneIntegralPowerBasis_gen {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ k} K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
              .subOneIntegralPowerBasis.gen = ζ - 1,
              noncomputable def IsPrimitiveRoot.subOneIntegralPowerBasis' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) :

              The integral PowerBasis of 𝓞 K given by ζ - 1, where K is a p-th cyclotomic extension of .

              Equations
              • .subOneIntegralPowerBasis' = .subOneIntegralPowerBasis
              Instances For
                @[simp]
                theorem IsPrimitiveRoot.subOneIntegralPowerBasis'_gen {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) :
                .subOneIntegralPowerBasis'.gen = .toInteger - 1
                theorem IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
                Prime (.toInteger - 1)

                ζ - 1 is prime if p ≠ 2 and ζ is a primitive p ^ (k + 1)-th root of unity. See zeta_sub_one_prime for a general statement.

                theorem IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [IsCyclotomicExtension {2 ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) :
                Prime (.toInteger - 1)

                ζ - 1 is prime if ζ is a primitive 2 ^ (k + 1)-th root of unity. See zeta_sub_one_prime for a general statement.

                theorem IsPrimitiveRoot.zeta_sub_one_prime {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) :
                Prime (.toInteger - 1)

                ζ - 1 is prime if ζ is a primitive p ^ (k + 1)-th root of unity.

                theorem IsPrimitiveRoot.zeta_sub_one_prime' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [h : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) :
                Prime (.toInteger - 1)

                ζ - 1 is prime if ζ is a primitive p-th root of unity.

                theorem IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) :
                Prime .subOneIntegralPowerBasis.gen
                theorem IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) :
                Prime .subOneIntegralPowerBasis'.gen
                theorem IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : } (hs : s k) (htwo : p ^ (k - s + 1) 2) :
                (Algebra.norm ) (.toInteger ^ p ^ s - 1) = p ^ p ^ s

                The norm, relative to , of ζ ^ p ^ s - 1 in a p ^ (k + 1)-th cyclotomic extension of is p ^ p ^ sifs ≤ kandp ^ (k - s + 1) ≠ 2`.

                theorem IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [IsCyclotomicExtension {2 ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) :
                (Algebra.norm ) (.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

                The norm, relative to , of ζ ^ 2 ^ k - 1 in a 2 ^ (k + 1)-th cyclotomic extension of is (-2) ^ 2 ^ k.

                theorem IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : } (hs : s k) (hodd : p 2) :
                (Algebra.norm ) (.toInteger ^ p ^ s - 1) = p ^ p ^ s

                The norm, relative to , of ζ ^ p ^ s - 1 in a p ^ (k + 1)-th cyclotomic extension of is p ^ p ^ s if s ≤ k and p ≠ 2.

                theorem IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
                (Algebra.norm ) (.toInteger - 1) = p

                The norm, relative to , of ζ - 1 in a p ^ (k + 1)-th cyclotomic extension of is p if p ≠ 2.

                theorem IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) (h : p 2) :
                (Algebra.norm ) (.toInteger - 1) = p

                The norm, relative to , of ζ - 1 in a p-th cyclotomic extension of is p if p ≠ 2.

                theorem IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (htwo : p ^ (k + 1) 2) :
                Prime ((Algebra.norm ) (.toInteger - 1))

                The norm, relative to , of ζ - 1 in a p ^ (k + 1)-th cyclotomic extension of is a prime if p ^ (k + 1) ≠ 2.

                theorem IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
                Prime ((Algebra.norm ) (.toInteger - 1))

                The norm, relative to , of ζ - 1 in a p ^ (k + 1)-th cyclotomic extension of is a prime if p ≠ 2.

                theorem IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) (hodd : p 2) :
                Prime ((Algebra.norm ) (.toInteger - 1))

                The norm, relative to , of ζ - 1 in a p-th cyclotomic extension of is a prime if p ≠ 2.

                theorem IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (htwo : p ^ (k + 1) 2) :
                ¬∃ (n : ), p .toInteger - n

                In a p ^ (k + 1)-th cyclotomic extension of , we have that ζ is not congruent to an integer modulo p if p ^ (k + 1) ≠ 2.

                theorem IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
                ¬∃ (n : ), p .toInteger - n

                In a p ^ (k + 1)-th cyclotomic extension of , we have that ζ is not congruent to an integer modulo p if p ≠ 2.

                theorem IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) (hodd : p 2) :
                ¬∃ (n : ), p .toInteger - n

                In a p-th cyclotomic extension of , we have that ζ is not congruent to an integer modulo p if p ≠ 2.

                theorem IsPrimitiveRoot.finite_quotient_span_sub_one {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) :
                theorem IsPrimitiveRoot.finite_quotient_span_sub_one' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) :
                theorem IsPrimitiveRoot.toInteger_sub_one_dvd_prime {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) :
                .toInteger - 1 p

                In a p ^ (k + 1)-th cyclotomic extension of , we have that ζ - 1 divides p in 𝓞 K.

                theorem IsPrimitiveRoot.toInteger_sub_one_dvd_prime' {p : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p} K] (hζ : IsPrimitiveRoot ζ p) :
                .toInteger - 1 p

                In a p-th cyclotomic extension of , we have that ζ - 1 divides p in 𝓞 K.

                theorem IsPrimitiveRoot.toInteger_sub_one_not_dvd_two {p : ℕ+} {k : } {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p 2) :
                ¬.toInteger - 1 2

                We have that hζ.toInteger - 1 does not divide 2.

                theorem IsCyclotomicExtension.Rat.absdiscr_prime_pow (p : ℕ+) (k : ) (K : Type u) [Field K] [CharZero K] [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ k} K] :
                NumberField.discr K = (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

                We compute the absolute discriminant of a p ^ k-th cyclotomic field. Beware that in the cases p ^ k = 1 and p ^ k = 2 the formula uses 1 / 2 = 0 and 0 - 1 = 0. See also the results below.

                theorem IsCyclotomicExtension.Rat.absdiscr_prime_pow_succ (p : ℕ+) (k : ) (K : Type u) [Field K] [CharZero K] [hp : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K] :
                NumberField.discr K = (-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

                We compute the absolute discriminant of a p ^ (k + 1)-th cyclotomic field. Beware that in the case p ^ k = 2 the formula uses 1 / 2 = 0. See also the results below.

                theorem IsCyclotomicExtension.Rat.absdiscr_prime (p : ℕ+) (K : Type u) [Field K] [CharZero K] [hp : Fact (Nat.Prime p)] [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.