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

State before:
a b c : ℤθ
⊢ ↑(unit ^ (-1)) = { f := 25, g := 13, h := 5 }
Tactic:
rfl
State after:
no goals