det_eq_det_toMatrix_of_finset — Mathlib

English

If there is a finite basis compatible with a Finset s, then det f equals the determinant of the matrix of f in that basis.

Русский

Если существует базис, связанный с конечным множеством s, то det f равно детерминанту матрицы представления f в этом базисе.

LaTeX

$$$\det f = \det(\mathrm{toMatrix}\, b\, b\, f)$ for some suitable finite basis $b$.$$

Lean4

theorem det_eq_det_toMatrix_of_finset [DecidableEq M] {s : Finset M} (b : Basis s A M) (f : M →ₗ[A] M) :
    LinearMap.det f = Matrix.det (LinearMap.toMatrix b b f) :=
  by
  have : ∃ s : Finset M, Nonempty (Basis s A M) := ⟨s, ⟨b⟩⟩
  rw [LinearMap.coe_det, dif_pos this, detAux_def'' _ b]

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