English
The equality ∥(x.zmodRepr)∥ = ∥x∥ is equivalent to ∥x∥ = 1 or x = 0.
Русский
Неравенство норм эквивалентно ∥x∥ = 1 или x = 0.
LaTeX
$$‖(x.zmodRepr)‖ = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0$$
Lean4
/-- `z - (toZMod z : ℤ_[p])` is contained in the maximal ideal of `ℤ_[p]`, for every `z : ℤ_[p]`.
The coercion from `ZMod p` to `ℤ_[p]` is `ZMod.cast`,
which coerces `ZMod p` into arbitrary rings.
This is unfortunate, but a consequence of the fact that we allow `ZMod p`
to coerce to rings of arbitrary characteristic, instead of only rings of characteristic `p`.
This coercion is only a ring homomorphism if it coerces into a ring whose characteristic divides
`p`. While this is not the case here we can still make use of the coercion.
-/
theorem toZMod_spec : x - (ZMod.cast (toZMod x) : ℤ_[p]) ∈ maximalIdeal ℤ_[p] :=
by
convert sub_zmodRepr_mem x using 2
dsimp [toZMod, toZModHom]
rcases Nat.exists_eq_add_of_lt hp_prime.1.pos with ⟨p', rfl⟩
change ↑((_ : ZMod (0 + p' + 1)).val) = (_ : ℤ_[0 + p' + 1])
rw [Nat.cast_inj]
apply mod_eq_of_lt
simpa only [zero_add] using zmodRepr_lt_p x
