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

State before:
P : 𝔽₂X
n : ℕ
⊢ P * Xpow n = Xpow n * P
Tactic:
rw [← XpowMul_eq_Xpow_mul, XpowMul_eq_mul_Xpow]
State after:
no goals

State before:
P P✝ Q✝ : 𝔽₂X
h : P * P✝ = P✝ * P
h0 : P * Q✝ = Q✝ * P
⊢ P * (P✝ + Q✝) = (P✝ + Q✝) * P
Tactic:
rw [𝔽₂X.add_mul, 𝔽₂X.mul_add, h, h0]
State after:
no goals