intCast_rightInverse — Mathlib

English

The cast from ZMod n to ℤ followed by Int.cast is a right inverse: ∀ z ∈ ℤ, z = (cast z : ZMod n).val.

Русский

Отображение ZMod n → ℤ затем обратно в ZMod n является правым обратным: ∀ z ∈ ℤ, z = (cast z : ZMod n).val.

LaTeX

$$$ \forall z \in \mathbb{Z}, \ z = \operatorname{val}((z : \mathrm{ZMod} n)) $$$

Lean4

theorem intCast_rightInverse : Function.RightInverse (cast : ZMod n → ℤ) ((↑) : ℤ → ZMod n) :=
  intCast_zmod_cast

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