det — Mathlib

English

The determinant of a unit matrix is itself a unit in the base ring.

Русский

Детерминант единичной матрицы является единицей в базовой кольцевой структуре.

LaTeX

$$The determinant map from GL_n(R) to units(R) is a monoid homomorphism.$$

Lean4

/-- The determinant of a unit matrix is itself a unit. -/
@[simps]
def det : GL n R →* Rˣ
    where
  toFun
    A :=
    { val := (↑A : Matrix n n R).det
      inv := (↑A⁻¹ : Matrix n n R).det
      val_inv := by rw [← det_mul, A.mul_inv, det_one]
      inv_val := by rw [← det_mul, A.inv_mul, det_one] }
  map_one' := Units.ext det_one
  map_mul' _ _ := Units.ext <| det_mul _ _

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