injective_toCircle — Mathlib

English

If T ≠ 0, the map toCircle: AddCircle T → Circle is injective.

Русский

Если T ≠ 0, отображение toCircle: AddCircle T → Circle инъективно.

LaTeX

$$$$ \text{If } T \neq 0,\ \operatorname{toCircle} \text{: Injective}. $$$$

Lean4

theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) :=
  by
  intro a b h
  induction a using QuotientAddGroup.induction_on
  induction b using QuotientAddGroup.induction_on
  simp_rw [toCircle_apply_mk] at h
  obtain ⟨m, hm⟩ := Circle.exp_eq_exp.mp h.symm
  rw [QuotientAddGroup.eq]; simp_rw [AddSubgroup.mem_zmultiples_iff, zsmul_eq_mul]
  use m
  field_simp at hm
  linarith

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