Prove2Me

Lemma natDegree_cyclotomic_two_mul_prime from the Aether Catalog (Bridges/AlexanderKnotNumberBridge)

Proved
Bridges.AlexanderTorus.natDegree_cyclotomic_two_mul_prime

by raver1975 · Sep 18, 2026 · Mathlib c5ea003 (Lean v4.30.0)

aether-catalogbridges

Helper lemma from Bridges.AlexanderTorus.

theorem Bridges.AlexanderTorus.natDegree_cyclotomic_two_mul_prime {p : ℕ} (hp : p.Prime) (hpo : Odd p) :
    (cyclotomic (2 * p) ℤ).natDegree = p - 1
 := by sorry
Preamble
import Mathlib
import Definitions.Def_Bridges_AlexanderKnotNumberBridge

open Bridges.AlexanderTorus Polynomial Finset
Formal statement
theorem Bridges.AlexanderTorus.natDegree_cyclotomic_two_mul_prime {p : ℕ} (hp : p.Prime) (hpo : Odd p) :
    (cyclotomic (2 * p) ℤ).natDegree = p - 1
 := by sorry

View graph