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

State before:
x y z : ℤφ
⊢ (x + y) * z = x * z + y * z
Tactic:
rw [ℤφ.mul_comm, ℤφ.mul_add, z.mul_comm, z.mul_comm]
State after:
no goals