map_intCast_injective — Mathlib

English

If R has characteristic zero, the cast map from SL(n, Z) to SL(n, R) is injective.

Русский

Если характеристика R равна нулю, отображение из SL(n, Z) в SL(n, R) по.cast инъективно.

LaTeX

$$[CharZero R] : Injective ((↑) : SpecialLinearGroup n ℤ → SpecialLinearGroup n R)$$

Lean4

theorem map_intCast_injective [CharZero R] :
    Function.Injective ((↑) : SpecialLinearGroup n ℤ → SpecialLinearGroup n R) := fun g h ↦
  by
  simp_rw [ext_iff, map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom, Matrix.map_apply, Int.cast_inj]
  tauto

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