∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (u : (NumberField.RingOfIntegers K)ˣ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K], (∃ n, (hζ.toInteger - 1) ^ 2 ∣ ↑u - ↑n) → u = 1 ∨ u = -1