toAddCircle_injective — Mathlib

English

Reiterated statement: the map from ZMod N to the additive circle is injective.

Русский

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

LaTeX

$$$$ \\mathrm{toAddCircle} \\text{ is injective.} $$$$

Lean4

theorem toAddCircle_injective : Function.Injective (toAddCircle : ZMod N → _) :=
  by
  intro x y hxy
  have : (0 : ℝ) < N := Nat.cast_pos.mpr (NeZero.pos _)
  rwa [toAddCircle_apply, toAddCircle_apply, AddCircle.coe_eq_coe_iff_of_mem_Ico, div_left_inj' this.ne', Nat.cast_inj,
      (val_injective N).eq_iff] at hxy <;>
    exact ⟨by positivity, by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _⟩

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