toZMod — Mathlib

English

zmodRepr x = 0 if and only if p divides x in ℤ_p.

Русский

zmodRepr(x) = 0 тогда и только тогда, когда p делит x в ℤ_p.

LaTeX

$$x.zmodRepr = 0 ↔ (p : ℤ_[p]) ∣ x$$

Lean4

/-- `toZMod` is a ring hom from `ℤ_[p]` to `ZMod p`,
with the equality `toZMod x = (zmodRepr x : ZMod p)`.
-/
def toZMod : ℤ_[p] →+* ZMod p :=
  toZModHom p zmodRepr
    (by
      rw [← maximalIdeal_eq_span_p]
      exact sub_zmodRepr_mem)
    (by
      rw [← maximalIdeal_eq_span_p]
      exact zmod_congr_of_sub_mem_max_ideal)

Похожие утверждения