toAddCircle_apply — Mathlib

English

The map from ZMod N to the additive circle is injective.

Русский

Отображение из ZMod N в аддитивный круг инъективно.

LaTeX

$$$$ \\mathrm{toAddCircle} : \\mathbb{Z}/N\\mathbb{Z} \\to \\mathrm{AddCircle}(p) \\text{ is injective}. $$$$

Lean4

/-- Explicit formula for `toCircle j`. Note that this is "evil" because it uses `ZMod.val`. Where
possible, it is recommended to lift `j` to `ℤ` and use `toAddCircle_intCast` instead.
-/
theorem toAddCircle_apply (j : ZMod N) : toAddCircle j = ↑(j.val / N : ℝ) := by
  rw [← toAddCircle_natCast, natCast_zmod_val]

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