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

State before:
n k : ℕ
⊢ XpowMul n (Xpow k) = Xpow k * Xpow n
Tactic:
rw [XpowMul_Xpow, Xpow_add]
State after:
no goals

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