mk_left_injective — Mathlib

English

Fix s ∈ ℕ+. The map m ↦ mk(m, s) is injective from M to DivisibleHull M; that is, if mk(m, s) = mk(n, s) then m = n.

Русский

Пусть фиксировано s ∈ ℕ+. Отображение m ↦ mk(m, s) инъективно из M в DivisibleHull M; если mk(m, s) = mk(n, s), то m = n.

LaTeX

$$$\\forall m,n\\in M (s\\in\\mathbb{N}_{>0}),\\; \\mathrm{mk}(m,s)=\\mathrm{mk}(n,s) \\Rightarrow m=n$.$$

Lean4

theorem mk_left_injective (s : ℕ+) : Function.Injective (fun (m : M) ↦ mk m s) :=
  by
  intro m n h
  simp_rw [mk_eq_mk_iff_smul_eq_smul] at h
  exact nsmul_right_injective (by simp) h

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