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

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