coe_inj — Mathlib

English

The canonical embedding of SL(2, ℤ) into GL(2, ℝ)⁺ is injective: if two elements have the same image, they are equal.

Русский

Каноническое вложение SL(2, ℤ) в GL(2, ℝ)⁺ инъективно: если образы двух элементов совпадают, то сами элементы равны.

LaTeX

$$$\operatorname{coe}(a) = \operatorname{coe}(b) \iff a = b$$$

Lean4

@[simp]
theorem coe_inj (a b : SL(2, ℤ)) : coe a = coe b ↔ a = b :=
  by
  refine ⟨fun h ↦ a.ext b fun i j ↦ ?_, congr_arg _⟩
  simp only [Subtype.ext_iff, GeneralLinearGroup.ext_iff] at h
  simpa [coe] using h i j

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