case h.e'_4.h.e'_6
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ↑(↑toZMod x) = ↑(zmodRepr x)
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ x - ↑(↑toZMod x) ∈ maximalIdeal ℤ_[p]
convert sub_zmodRepr_mem x using 2
case h.e'_4.h.e'_6
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ↑↑(zmodRepr x) = ↑(zmodRepr x)
case h.e'_4.h.e'_6
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ↑(↑toZMod x) = ↑(zmodRepr x)
dsimp [toZMod, toZModHom]
case h.e'_4.h.e'_6.intro
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ↑↑(zmodRepr x) = ↑(zmodRepr x)
case h.e'_4.h.e'_6
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ↑↑(zmodRepr x) = ↑(zmodRepr x)
rcases exists_eq_add_of_lt hp_prime.1.pos with ⟨p', rfl⟩
case h.e'_4.h.e'_6.intro
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ↑(ZMod.val ↑(zmodRepr x)) = ↑(zmodRepr x)
case h.e'_4.h.e'_6.intro
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ↑↑(zmodRepr x) = ↑(zmodRepr x)
change ↑((_ : ZMod (0 + p' + 1)).val) = (_ : ℤ_[0 + p' + 1])
case h.e'_4.h.e'_6.intro
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ zmodRepr x % (p' + 1) = zmodRepr x
case h.e'_4.h.e'_6.intro
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ↑(ZMod.val ↑(zmodRepr x)) = ↑(zmodRepr x)
simp only [ZMod.val_nat_cast, add_zero, add_def, Nat.cast_inj, zero_add]
case h.e'_4.h.e'_6.intro.h
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ zmodRepr x < p' + 1
case h.e'_4.h.e'_6.intro
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ zmodRepr x % (p' + 1) = zmodRepr x
apply mod_eq_of_lt
no goals
case h.e'_4.h.e'_6.intro.h
r : ℚ
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ zmodRepr x < p' + 1
simpa only [zero_add] using zmodRepr_lt_p x