det_reindex_symm — Mathlib

English

For a bijection e: ι' ≃ ι, the determinant after reindexing by e.symm with v ∘ e equals the determinant with v: (b.reindex e.symm).det (v ∘ e) = b.det v.

Русский

Для биекции e.symm: ι' ≃ ι детерминант после перестановки по e.symm с v ∘ e равен детерминанту исходного базиса: (b.reindex e.symm).det (v ∘ e) = b.det v.

LaTeX

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

Lean4

theorem det_reindex_symm {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (v : ι → M) (e : ι' ≃ ι) :
    (b.reindex e.symm).det (v ∘ e) = b.det v := by
  rw [det_reindex, Function.comp_assoc, e.self_comp_symm, Function.comp_id]

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