no goals
p : ℕ
R : Type u_1
S : Type ?u.743877
T : Type ?u.743880
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type ?u.743895
β : Type ?u.743898
x y : 𝕎 R
⊢ WittVector.ghostFun (-x) = -WittVector.ghostFun x
ghost_fun_tac -X 0, ![x.coeff]