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

State before:
a b c : ℤθ
⊢ ↑(unit ^ (-3)) = { f := 10591, g := 5553, h := 2139 }
Tactic:
norm_cast
State after:
no goals