isUnit_iff_isUnit_det — Mathlib

English

For finite free modules, a linear map is a unit iff its determinant is a unit.

Русский

Для конечномерного свободного модуля линейное отображение является единицей тогда и только тогда, когда детерминант является единицей.

LaTeX

$$$\text{IsUnit}(f) \iff \text{IsUnit}(\det f)$$$

Lean4

theorem isUnit_iff_isUnit_det [Module.Finite R M] [Module.Free R M] (f : M →ₗ[R] M) : IsUnit f ↔ IsUnit f.det :=
  by
  let b := Module.Free.chooseBasis R M
  rw [← isUnit_toMatrix_iff b, ← det_toMatrix b, Matrix.isUnit_iff_isUnit_det (toMatrix b b f)]

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