det_toMatrix_prod — Mathlib

English

The determinant of the product of a list of transvection matrices is 1: det((L.map toMatrix).prod) = 1.

Русский

Определитель произведения списка матриц трансвеκций равен 1: det((L.map toMatrix).prod) = 1.

LaTeX

$$$\\det\\left(\\left(\\operatorname{map}\\toMatrix\\,L\\right).prod\\right) = 1$$$

Lean4

@[simp]
theorem det_toMatrix_prod [Fintype n] (L : List (TransvectionStruct n 𝕜)) : det (L.map toMatrix).prod = 1 := by
  induction L with
  | nil => simp
  | cons _ _ IH => simp [IH]

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