isUnit_det — Mathlib

English

If f is an isomorphism (linear equivalence), then det(toMatrix v v' f) is a unit.

Русский

Если f — линейное изоморфизм, то детерминант соответствующей матрицы является единицей (элементом единицы кольца).

LaTeX

$$IsUnit( det( toMatrix v v' f ) )$$

Lean4

theorem isUnit_det (f : M ≃ₗ[R] M') (v : Basis ι R M) (v' : Basis ι R M') : IsUnit (LinearMap.toMatrix v v' f).det :=
  by
  apply isUnit_det_of_left_inverse
  simpa using (LinearMap.toMatrix_comp v v' v f.symm f).symm

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