A divisor of an odd number is odd
ProvedBridges.AlexanderTorus.odd_of_dvd_oddaether-catalogbridges
A divisor of an odd number is odd.
theorem Bridges.AlexanderTorus.odd_of_dvd_odd {N d : ℕ} (hN : Odd N) (hd : d ∣ N) : Odd d := by sorry
Formalization Note Helper lemma from the Aether Catalog source Bridges/AlexanderKnotNumberBridge.lean (namespace Bridges.AlexanderTorus); statement byte-identical to the source declaration.
Preamble
import Mathlib
Formal statement
theorem Bridges.AlexanderTorus.odd_of_dvd_odd {N d : ℕ} (hN : Odd N) (hd : d ∣ N) : Odd d := by sorry