p : ℕ
R : Type ?u.168255
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m n : ℕ
⊢ ↑constantCoeff (m • X 0) = 0
p : ℕ
R : Type ?u.168255
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m n : ℕ
⊢ ↑constantCoeff (wittNSMul p m n) = 0
apply constantCoeff_wittStructureInt p _ _ n
no goals
p : ℕ
R : Type ?u.168255
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m n : ℕ
⊢ ↑constantCoeff (m • X 0) = 0
simp only [smul_zero, map_nsmul, constantCoeff_X]