injective_valMinAbs

Mathlib.Data.ZMod.ValMinAbs

URI: https://scilib.ai/kg/mathlib#ZMod.injective_valMinAbs

English

The map from ZMod n to the integers given by x ↦ x.valMinAbs is injective.

Русский

Отображение x ↦ x.valMinAbs: ZMod n → ℤ инъективно.

LaTeX

$$$\\mathrm{Injective}(\\mathrm{valMinAbs} : \\mathbb{Z}/n\\mathbb{Z} \\to \\mathbb{Z})$$$

Lean4

theorem injective_valMinAbs : (valMinAbs : ZMod n → ℤ).Injective :=
  Function.injective_iff_hasLeftInverse.2 ⟨_, coe_valMinAbs⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru