basisFun_det_apply — Mathlib

English

The determinant after reindexing by an equivalence between index sets equals the determinant of the original basis under the corresponding equivalence.

Русский

Детерминант после перенумерации эквивалентностью между наборами индексов равен детерминанту исходного базиса под соответствующей эквиваленцией.

LaTeX

$$det_reindex' (b : Basis ι R M) (e : ι ≃ ι') : (b.reindex e).det = b.det.domDomCongr e$$

Lean4

theorem basisFun_det_apply (v : ι → ι → R) : (Pi.basisFun R ι).det v = (Matrix.of v).det :=
  by
  rw [Pi.basisFun_det]
  rfl

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