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