Lemma alexander_not_irreducible_of_not_prime from the Aether Catalog (Bridges/AlexanderKnotNumberBridge)

Proved

Bridges.AlexanderTorus.alexander_not_irreducible_of_not_prime

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

aether-catalogbridges

Helper lemma from Bridges.AlexanderTorus.

theorem Bridges.AlexanderTorus.alexander_not_irreducible_of_not_prime {N : ℕ} (hN : Odd N) (h1 : 1 < N)
    (hnp : ¬ N.Prime) : ¬ Irreducible (alexander N)
 := by sorry

Preamble

import Mathlib
import Definitions.Def_Bridges_AlexanderKnotNumberBridge

open Bridges.AlexanderTorus Polynomial Finset

Formal statement

theorem Bridges.AlexanderTorus.alexander_not_irreducible_of_not_prime {N : ℕ} (hN : Odd N) (h1 : 1 < N)
    (hnp : ¬ N.Prime) : ¬ Irreducible (alexander N)
 := by sorry

View graph