intCast_surjective — Mathlib

English

Let n be a natural number. The reduction map from the integers to ZMod n sending x to x modulo n is surjective.

Русский

Пусть n — натуральное число. Отображение из \u211d в ZMod n, отправляющее x в его остаток по модулю n, сюръективно.

LaTeX

$$$\\\\forall y \\\\in \\\\mathbb{Z}/n\\\\mathbb{Z}, \\\\exists x \\\\in \\\\mathbb{Z}, x \\\\equiv y \\\\pmod{n}$$$

Lean4

theorem intCast_surjective : Function.Surjective ((↑) : ℤ → ZMod n) :=
  intCast_rightInverse.surjective

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