detAux_def' — Mathlib

English

The determinant of LinearMap.toMatrix does not depend on the choice of basis.

Русский

Детерминант LinearMap.toMatrix не зависит от выбора базиса.

LaTeX

$$det (LinearMap.toMatrix b b f) = det (LinearMap.toMatrix c c f)$$

Lean4

/-- Unfold lemma for `detAux`.

See also `detAux_def''` which allows you to vary the basis.
-/
theorem detAux_def' (b : Basis ι A M) (f : M →ₗ[A] M) :
    LinearMap.detAux (Trunc.mk b) f = Matrix.det (LinearMap.toMatrix b b f) :=
  by
  rw [detAux]
  rfl

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