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

State before:
P : 𝔽₂X
n : ℕ
⊢ (P * Xpow n).square = P.square * (Xpow n).square
Tactic:
rw [← XpowMul_eq_mul_Xpow, square_XpowMul,
square_Xpow, XpowMul_eq_mul_Xpow]
State after:
no goals

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