map_intCast_inj — Mathlib

English

For CharZero R, the cast from SL(n, Z) to SL(n, R) is an embedding: equality of images implies equality of original elements.

Русский

Для CharZero R отображение из SL(n, Z) в SL(n, R) является вложением: равенство образов следует из равенства самих элементов.

LaTeX

$$[CharZero R] {x y : SpecialLinearGroup n ℤ} : (x : SpecialLinearGroup n R) = y ↔ x = y$$

Lean4

@[simp]
theorem map_intCast_inj [CharZero R] {x y : SpecialLinearGroup n ℤ} : (x : SpecialLinearGroup n R) = y ↔ x = y :=
  map_intCast_injective.eq_iff

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