Theorem: IMOSL.IMO2012A5.ℤφ.one_mul (IMOSLLean4/IMO2012/A5/Extra/ExplicitRings/Zphi.lean)

State before:
a b : ℤ
⊢ 1 * { re := a, im := b } = { re := a, im := b }
Tactic:
rw [mul_def, one_def, one_mul, one_mul,
zero_mul, mul_zero, add_zero, add_zero, add_zero]
State after:
no goals