Theorem: IMOSL.IMO2012A5.𝔽₃.add_mul (IMOSLLean4/IMO2012/A5/Extra/ExplicitRings/F3.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