det_reindex — Mathlib

English

If b is a basis, v: ι' → M, and e is a bijection ι ≃ ι', then the determinant under reindexing satisfies (b.reindex e).det v = b.det (v ∘ e).

Русский

Если b — базис, v : ι' → M, и e — биекция ι ≃ ι', то детерминант при перераспределении индексов: (b.reindex e).det v = b.det (v ∘ e).

LaTeX

$$(b.reindex e).det v = b.det (v ∘ e)$$

Lean4

theorem det_reindex {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
    (b.reindex e).det v = b.det (v ∘ e) := by rw [det_apply, toMatrix_reindex', det_reindexAlgEquiv, det_apply]

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