p : ℕ
R : Type ?u.144931
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (-X 0) = 0
p : ℕ
R : Type ?u.144931
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (wittNeg p n) = 0
apply constantCoeff_wittStructureInt p _ _ n
no goals
p : ℕ
R : Type ?u.144931
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (-X 0) = 0
simp only [neg_zero, RingHom.map_neg, constantCoeff_X]