injective_toCircle

Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

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

English

For all N>0, the map toCircle: ZMod N → Circle is injective.

Русский

Для любого N>0 отображение toCircle: ZMod N → Circle инъективно.

LaTeX

$$$\\mathrm{Injective}(\\mathrm{toCircle} : ZMod(N) \\to Circle)$$$

Lean4

theorem injective_toCircle : Injective (toCircle : ZMod N → Circle) :=
  (AddCircle.injective_toCircle one_ne_zero).comp (toAddCircle_injective N)

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

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

Разделы

Аффилиация

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