coe_matrix_coe — Mathlib

English

The symmetric of toLin' mapped to linear map equals the linear map of the inverse element.

Русский

Симметрия toLin' в отображение в линейное отображение равна линейному отображению обратного элемента.

LaTeX

$$↑A.toLin'.symm = Matrix.toLin'(↑ₘA^{-1})$$

Lean4

@[simp]
theorem coe_matrix_coe (g : SpecialLinearGroup n ℤ) :
    ↑(g : SpecialLinearGroup n R) = (↑g : Matrix n n ℤ).map (Int.castRingHom R) :=
  map_apply_coe (Int.castRingHom R) g

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