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

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