case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ x ∈ RingHom.ker toZMod ↔ x ∈ maximalIdeal ℤ_[p]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ RingHom.ker toZMod = maximalIdeal ℤ_[p]
ext x
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ↑toZMod x = 0 ↔ x ∈ maximalIdeal ℤ_[p]
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ x ∈ RingHom.ker toZMod ↔ x ∈ maximalIdeal ℤ_[p]
rw [RingHom.mem_ker]
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ↑toZMod x = 0 → x ∈ maximalIdeal ℤ_[p]

case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ x ∈ maximalIdeal ℤ_[p] → ↑toZMod x = 0
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ↑toZMod x = 0 ↔ x ∈ maximalIdeal ℤ_[p]
constructor
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : ↑toZMod x = 0
⊢ x ∈ maximalIdeal ℤ_[p]
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ↑toZMod x = 0 → x ∈ maximalIdeal ℤ_[p]
intro h
no goals
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : ↑toZMod x = 0
⊢ x ∈ maximalIdeal ℤ_[p]
simpa only [h, ZMod.cast_zero, sub_zero] using toZMod_spec x
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x ∈ maximalIdeal ℤ_[p]
⊢ ↑toZMod x = 0
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ x ∈ maximalIdeal ℤ_[p] → ↑toZMod x = 0
intro h
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ ↑toZMod x = 0
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x ∈ maximalIdeal ℤ_[p]
⊢ ↑toZMod x = 0
rw [← sub_zero x] at h
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ ↑(zmodRepr x) = 0
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ ↑toZMod x = 0
dsimp [toZMod, toZModHom]
case h.e'_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ 0 = ↑0

case h.mpr.convert_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ x - ↑(zmodRepr x) ∈ maximalIdeal ℤ_[p]
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ ↑(zmodRepr x) = 0
convert zmod_congr_of_sub_mem_max_ideal x _ 0 _ h
case h.mpr.convert_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ x - ↑(zmodRepr x) ∈ maximalIdeal ℤ_[p]
case h.e'_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ 0 = ↑0

case h.mpr.convert_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ x - ↑(zmodRepr x) ∈ maximalIdeal ℤ_[p]
norm_cast
no goals
case h.mpr.convert_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ x - ↑(zmodRepr x) ∈ maximalIdeal ℤ_[p]
apply sub_zmodRepr_mem