coe_GLPos_coe_GL_coe_matrix — Mathlib

English

Coercions from SpecialLinearGroup to GLPos to GL to Matrix are compatible: the triple-coercion of g yields the same underlying matrix as directly coercing g to Matrix.

Русский

Приведения из SpecialLinearGroup через GLPos и далее в GL и затем в Matrix согласованы: тройное приведение g даёт ту же матрицу, что и прямое приведение g к Matrix.

LaTeX

$$$(↑(↑(↑g : GLPos n R) : GL n R) : Matrix n n R) = ↑g.$$$

Lean4

/-- Coercing a `Matrix.SpecialLinearGroup` via `GL_pos` and `GL` is the same as coercing straight to
a matrix. -/
@[simp]
theorem coe_GLPos_coe_GL_coe_matrix (g : SpecialLinearGroup n R) :
    (↑(↑(↑g : GLPos n R) : GL n R) : Matrix n n R) = ↑g :=
  rfl

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