det_map' — Mathlib

English

The determinant of a mapped basis equals the determinant of the original basis composed with the inverse linear map.

Русский

Детерминант базиса после отображения равен детерминанту исходного базиса, композиционно сообразному с обратным линейным отображением.

LaTeX

$$(b.map f).det = b.det.compLinearMap f.symm$$

Lean4

theorem det_map' (b : Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).det = b.det.compLinearMap f.symm :=
  AlternatingMap.ext <| b.det_map f

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