map_det — Mathlib

English

The determinant commutes with the base-change map: det(map f g) = Units.map f (det g).

Русский

Определитель после отображения совместим с базовым изменением: det(map f g) = Units.map f(det g).

LaTeX

$$\\det(\\mathrm{map}\\,f\\,g) = \\mathrm{Units.map}\\,f\\bigl( \\det g \\bigr)$$

Lean4

protected theorem map_det (g : GL n R) :
    Matrix.GeneralLinearGroup.det (map f g) = Units.map f (Matrix.GeneralLinearGroup.det g) :=
  by
  ext
  simp only [map, Matrix.GeneralLinearGroup.val_det_apply, Units.coe_map, MonoidHom.coe_coe]
  exact Eq.symm (RingHom.map_det f g.1)

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