isUnit_det — Mathlib

English

If an endomorphism f is invertible, then its determinant is a unit in the base ring.

Русский

Если эндоморфизм f обратим, то det f — единичный элемент в базовом кольце.

LaTeX

$$$\text{If } f \text{ is invertible, then } \det f \in A^\times$$$

Lean4

/-- If a linear map is invertible, so is its determinant. -/
theorem isUnit_det {A : Type*} [CommRing A] [Module A M] (f : M →ₗ[A] M) (hf : IsUnit f) : IsUnit (LinearMap.det f) :=
  IsUnit.map LinearMap.det hf

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