no goals
p : ℕ
R : Type u_1
S : Type ?u.801752
T : Type ?u.801755
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type ?u.801770
β : Type ?u.801773
x y : 𝕎 R
m : ℤ
⊢ WittVector.ghostFun (m • x) = m • WittVector.ghostFun x
ghost_fun_tac m • (X 0 : MvPolynomial _ ℤ), ![x.coeff]