theorem
IsCyclotomicExtension.Rat.zeta_sub_one_prime
{K : Type u_1}
[Field K]
{ζ : K}
{p : ℕ+}
{k : ℕ}
[hp : Fact (Nat.Prime ↑p)]
[CharZero K]
[IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
(hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1)))
(hodd : p ≠ 2)
:
Prime { val := ζ - 1, property := (_ : ζ - 1 ∈ NumberField.ringOfIntegers K) }
theorem
IsCyclotomicExtension.Rat.zeta_sub_one_prime'
{K : Type u_1}
[Field K]
{ζ : K}
{p : ℕ+}
[hp : Fact (Nat.Prime ↑p)]
[CharZero K]
[h : IsCyclotomicExtension {p} ℚ K]
(hζ : IsPrimitiveRoot ζ ↑p)
(hodd : p ≠ 2)
:
Prime { val := ζ - 1, property := (_ : ζ - 1 ∈ NumberField.ringOfIntegers K) }