English
The norm of zmodRepr(x) equals the norm of x or equals 1 depending on whether x is zero or a unit; more precisely, ∥(x.zmodRepr)∥ = ∥x∥ implies ∥x∥ = 1 or x = 0.
Русский
Норма ∥(x.zmodRepr)∥ равна ∥x∥ либо равно 1, если x не нулевой и не является нулём.
LaTeX
$$‖(x.zmodRepr)‖ = ‖x‖ → (‖x‖ = 1 ∨ x = 0)$$
Lean4
/-- `toZModHom` is an auxiliary constructor for creating ring homs from `ℤ_[p]` to `ZMod v`.
-/
def toZModHom (v : ℕ) (f : ℤ_[p] → ℕ) (f_spec : ∀ x, x - f x ∈ (Ideal.span {↑v} : Ideal ℤ_[p]))
(f_congr :
∀ (x : ℤ_[p]) (a b : ℕ),
x - a ∈ (Ideal.span {↑v} : Ideal ℤ_[p]) → x - b ∈ (Ideal.span {↑v} : Ideal ℤ_[p]) → (a : ZMod v) = b) :
ℤ_[p] →+* ZMod v where
toFun x := f x
map_zero' := by
rw [f_congr (0 : ℤ_[p]) _ 0, cast_zero]
· exact f_spec _
· simp only [sub_zero, cast_zero, Submodule.zero_mem]
map_one' := by
rw [f_congr (1 : ℤ_[p]) _ 1, cast_one]
· exact f_spec _
· simp only [sub_self, cast_one, Submodule.zero_mem]
map_add' := by
intro x y
rw [f_congr (x + y) _ (f x + f y), cast_add]
· exact f_spec _
· convert Ideal.add_mem _ (f_spec x) (f_spec y) using 1
rw [cast_add]
ring
map_mul' := by
intro x y
rw [f_congr (x * y) _ (f x * f y), cast_mul]
· exact f_spec _
· let I : Ideal ℤ_[p] := Ideal.span {↑v}
convert I.add_mem (I.mul_mem_left x (f_spec y)) (I.mul_mem_right ↑(f y) (f_spec x)) using 1
rw [cast_mul]
ring
