Theorem: ℤα.my_map_one (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
⊢ toℂ one = 1
Tactic:
simp only [toℂ, one]
State after:
a b c : ℤα
⊢ ↑1 + ↑0 * complexα = 1

State before:
a b c : ℤα
⊢ ↑1 + ↑0 * complexα = 1
Tactic:
norm_num
State after:
no goals