case a
p : ℕ
R : Type ?u.41310
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittZero p n) = ↑(map (Int.castRingHom ℚ)) 0
p : ℕ
R : Type ?u.41310
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ wittZero p n = 0
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
no goals
case a
p : ℕ
R : Type ?u.41310
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittZero p n) = ↑(map (Int.castRingHom ℚ)) 0
simp only [wittZero, wittStructureRat, bind₁, aeval_zero', constantCoeff_xInTermsOfW,
  RingHom.map_zero, AlgHom.map_zero, map_wittStructureInt]