toAddCircle_inj — Mathlib

English

Let N be a positive integer. The map j mod N → toAddCircle(j) into the circle is injective; equivalently, for all j,k ∈ ZMod N, if toAddCircle j = toAddCircle k then j = k.

Русский

Пусть N — положительное целое число. Отображение j mod N → toAddCircle(j) в окружность является инъективным; то есть для любых j, k ∈ ZMod N выполняется toAddCircle j = toAddCircle k тогда и только если j = k.

LaTeX

$$$ \forall N\ [N \neq 0],\ \forall j,k \in \mathbb{Z}/N\mathbb{Z},\ \operatorname{toAddCircle}(j) = \operatorname{toAddCircle}(k) \iff j = k. $$$

Lean4

@[simp]
theorem toAddCircle_inj {j k : ZMod N} : toAddCircle j = toAddCircle k ↔ j = k :=
  (toAddCircle_injective N).eq_iff

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