basisFun_det — Mathlib

English

Repeating det_reindex: the determinant under a reindexing by a bijection equals the determinant with the composed index map.

Русский

Повтор det_reindex: детерминант после перенумерации равен детерминанту с композиции индексов.

LaTeX

$$det_reindex _ _$$

Lean4

@[simp]
theorem basisFun_det : (Pi.basisFun R ι).det = Matrix.detRowAlternating :=
  by
  ext M
  rw [Basis.det_apply, Basis.coePiBasisFun.toMatrix_eq_transpose, det_transpose]

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