Theorem: ℤω.my_map_one (Mordell4/Eisenstein.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