det_reindex' — Mathlib

English

The determinant after reindexing equals the original determinant composed with an equivalence on indices.

Русский

Детерминант после перенумерации равен исходному детерминанту, скомпонованному с эквивалентностью индексов.

LaTeX

$$ (b.reindex e).det = b.det.domDomCongr e$$

Lean4

theorem det_reindex' {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (e : ι ≃ ι') :
    (b.reindex e).det = b.det.domDomCongr e :=
  AlternatingMap.ext fun _ => det_reindex _ _ _

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