discr_reindex — Mathlib

English

Discriminant is preserved under a basis reindexing by an equivalence of index sets: discr A (b ∘ φ) = discr A b.

Русский

Дискриминант сохраняется при замене базиса по биекции индексов: дискриминант не меняется при перестановке индексов.

LaTeX

$$discr A (b ∘ φ) = discr A b$$

Lean4

@[simp]
theorem discr_reindex (b : Basis ι A B) (f : ι ≃ ι') : discr A (b ∘ ⇑f.symm) = discr A b := by
  classical rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]

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