p : ℕ
R : Type ?u.1978909
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑constantCoeff (wittStructureInt p Φ 0) = ↑constantCoeff Φ
p : ℕ
R : Type ?u.1978909
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ ↑constantCoeff (wittStructureInt p Φ 0) = ↑constantCoeff Φ
have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp
case a
p : ℕ
R : Type ?u.1978909
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑(Int.castRingHom ℚ) (↑constantCoeff (wittStructureInt p Φ 0)) = ↑(Int.castRingHom ℚ) (↑constantCoeff Φ)
p : ℕ
R : Type ?u.1978909
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑constantCoeff (wittStructureInt p Φ 0) = ↑constantCoeff Φ
apply inj
no goals
case a
p : ℕ
R : Type ?u.1978909
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑(Int.castRingHom ℚ) (↑constantCoeff (wittStructureInt p Φ 0)) = ↑(Int.castRingHom ℚ) (↑constantCoeff Φ)
rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero,
  constantCoeff_map]
p : ℕ
R : Type ?u.1978909
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
m n : ℤ
⊢ ↑(Int.castRingHom ℚ) m = ↑(Int.castRingHom ℚ) n → m = n
p : ℕ
R : Type ?u.1978909
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ Function.Injective ↑(Int.castRingHom ℚ)
intro m n
no goals
p : ℕ
R : Type ?u.1978909
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
m n : ℤ
⊢ ↑(Int.castRingHom ℚ) m = ↑(Int.castRingHom ℚ) n → m = n
exact Int.cast_inj.mp