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