Lemma X_add_one_mul_alexander_odd from the Aether Catalog (Bridges/AlexanderKnotNumberBridge)
ProvedBridges.AlexanderTorus.X_add_one_mul_alexander_oddaether-catalogbridges
Helper lemma from Bridges.AlexanderTorus.
theorem Bridges.AlexanderTorus.X_add_one_mul_alexander_odd {N : ℕ} (hN : Odd N) :
(X + 1) * alexander N = X ^ N + 1
:= by sorry
Preamble
import Mathlib import Definitions.Def_Bridges_AlexanderKnotNumberBridge open Bridges.AlexanderTorus Polynomial Finset
Formal statement
theorem Bridges.AlexanderTorus.X_add_one_mul_alexander_odd {N : ℕ} (hN : Odd N) :
(X + 1) * alexander N = X ^ N + 1
:= by sorry