det_toMatrix' — Mathlib

English

The determinant of a linear map equals the determinant of the corresponding matrix given by toMatrix' in a compatible setting.

Русский

Детерминант линейного отображения равен детерминанту соответствующей матрицы, заданной toMatrix' в совместимой ситуации.

LaTeX

$$$\det(\mathrm{toMatrix}'\, f) = \det f$$$

Lean4

@[simp]
theorem det_toMatrix' {ι : Type*} [Fintype ι] [DecidableEq ι] (f : (ι → A) →ₗ[A] ι → A) :
    Matrix.det (LinearMap.toMatrix' f) = LinearMap.det f := by simp [← toMatrix_eq_toMatrix']

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