Theorem: ℤθ.units_are (Mordell4/CubicRing.lean)

State before:
a✝ b c : ℤθ
a : ℤθˣ
⊢ ∃ n, a = unit ^ n ∨ a = -unit ^ n
Tactic:
sorry
State after:
no goals