Theorem: IMOSL.IMO2012A5.𝔽₂X.mul_XpowMul_right (IMOSLLean4/Extra/F2X/Defs.lean)

State before:
n : ℕ
P Q : 𝔽₂X
⊢ P * XpowMul n Q = XpowMul n (P * Q)
Tactic:
rw [P.mul_comm, mul_XpowMul_left, Q.mul_comm]
State after:
no goals