Lemma alexander_semiprime_factor_data from the Aether Catalog (Bridges/AlexanderKnotNumberBridge)

Proved

Bridges.AlexanderTorus.alexander_semiprime_factor_data

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

aether-catalogbridges

Helper lemma from Bridges.AlexanderTorus.

theorem Bridges.AlexanderTorus.alexander_semiprime_factor_data {p q : ℕ} (hp : p.Prime) (hq : q.Prime)
    (hpo : Odd p) (hqo : Odd q) (hne : p ≠ q) :
    (cyclotomic (2 * p) ℤ).natDegree = p - 1 ∧
    (cyclotomic (2 * q) ℤ).natDegree = q - 1 ∧
    (cyclotomic (2 * (p * q)) ℤ).natDegree = (p - 1) * (q - 1) ∧
    Irreducible (cyclotomic (2 * p) ℤ) ∧ Irreducible (cyclotomic (2 * q) ℤ) ∧
    Irreducible (cyclotomic (2 * (p * q)) ℤ)
 := by sorry

Preamble

import Mathlib
import Definitions.Def_Bridges_AlexanderKnotNumberBridge

open Bridges.AlexanderTorus Polynomial Finset

Formal statement

theorem Bridges.AlexanderTorus.alexander_semiprime_factor_data {p q : ℕ} (hp : p.Prime) (hq : q.Prime)
    (hpo : Odd p) (hqo : Odd q) (hne : p ≠ q) :
    (cyclotomic (2 * p) ℤ).natDegree = p - 1 ∧
    (cyclotomic (2 * q) ℤ).natDegree = q - 1 ∧
    (cyclotomic (2 * (p * q)) ℤ).natDegree = (p - 1) * (q - 1) ∧
    Irreducible (cyclotomic (2 * p) ℤ) ∧ Irreducible (cyclotomic (2 * q) ℤ) ∧
    Irreducible (cyclotomic (2 * (p * q)) ℤ)
 := by sorry

View graph