det_toLin — Mathlib

English

Under existence of a finite-basis basis for a Finite Finset, det f equals the determinant of the matrix of f in that basis (via a more general finset-based statement).

Русский

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

LaTeX

$$$\det f = \det(\mathrm{toMatrix}\, b\, b\, f)$ for a Basis $b$ associated with a Finite Finset.$$

Lean4

@[simp]
theorem det_toLin (b : Basis ι R M) (f : Matrix ι ι R) : LinearMap.det (Matrix.toLin b b f) = f.det := by
  rw [← LinearMap.det_toMatrix b, LinearMap.toMatrix_toLin]

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