map_mapGL — Mathlib

English

The matrix corresponding to mapGL g equals the original special linear matrix g in matrix form over S.

Русский

Соответствие матрицы mapGL g равно исходной матрице SpecialLinearGroup g в виде матрицы над S.

LaTeX

$$\\bigl( (\\mathrm{mapGL}\\, g) : \\mathrm{Matrix}_{n\\times n} S \\bigr) = g.map( \\mathrm{algebraMap}\\, R\\ S )$$

Lean4

@[simp]
theorem map_mapGL {T : Type*} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
    (g : SpecialLinearGroup n R) : (mapGL S g).map (algebraMap S T) = mapGL T g :=
  by
  ext
  simp [IsScalarTower.algebraMap_apply R S T]

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