case a
p : ℕ
R : Type ?u.44782
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittOne p 0) = ↑(map (Int.castRingHom ℚ)) 1
p : ℕ
R : Type ?u.44782
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittOne p 0 = 1
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
no goals
case a
p : ℕ
R : Type ?u.44782
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittOne p 0) = ↑(map (Int.castRingHom ℚ)) 1
simp only [wittOne, wittStructureRat, xInTermsOfW_zero, AlgHom.map_one, RingHom.map_one,
  bind₁_X_right, map_wittStructureInt]