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

State before:
n : ℕ
P : 𝔽₂X
k : ℕ
⊢ XpowMul n P * Xpow k = XpowMul n (P * Xpow k)
Tactic:
rw [← XpowMul_eq_mul_Xpow, ← XpowMul_eq_mul_Xpow,
← XpowMul_nat_add, ← XpowMul_nat_add, Nat.add_comm]
State after:
no goals

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