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

State before:
a b c : ℤθ
⊢ (↑(unit ^ 1)).f % 3 = 2 ∧ (↑(unit ^ 1)).g % 3 = 0 ∧ (↑(unit ^ 1)).h % 3 = 2
Tactic:
norm_cast
State after:
no goals