zmodRepr_spec — Mathlib

English

For any p prime and x ∈ ℤ_p, the pair (zmodRepr x, x) satisfies that zmodRepr x < p and x − zmodRepr x lies in the maximal ideal of ℤ_p.

Русский

Пусть p — простое число и x ∈ ℤ_p. Число zmodRepr(x) удовлетворяет zmodRepr(x) < p и x − zmodRepr(x) ∈ maximalIdeal(ℤ_p).

LaTeX

$$$zmodRepr(x) < p \land x - zmodRepr(x) \in \mathfrak{m}_{\mathbb{Z}_{(p)}}$$$

Lean4

theorem zmodRepr_spec : zmodRepr x < p ∧ x - zmodRepr x ∈ maximalIdeal ℤ_[p] :=
  Classical.choose_spec (existsUnique_mem_range x).exists

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