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