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

State before:
a b c : ℤθ
⊢ ↑unit = { f := -1, g := -3, h := -1 }
Tactic:
rfl
State after:
no goals