chore(LinearAlgebra): golf entire isUnit_det (leanprover-community#28438)

Author: euprunin

Mathlib/LinearAlgebra/Determinant.lean

@@ -299,11 +299,7 @@ theorem det_conj {N : Type*} [AddCommGroup N] [Module A N] (f : M →ₗ[A] M) (
 
 /-- 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) := by
-  obtain ⟨g, hg⟩ : ∃ g, f.comp g = 1 := hf.exists_right_inv
-  have : LinearMap.det f * LinearMap.det g = 1 := by
-    simp only [← LinearMap.det_comp, hg, MonoidHom.map_one]
-  exact isUnit_of_mul_eq_one _ _ this
+    IsUnit (LinearMap.det f) := IsUnit.map LinearMap.det hf
 
 /-- If a linear map has determinant different from `1`, then the space is finite-dimensional. -/
 theorem finiteDimensional_of_det_ne_one {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] (f : M →ₗ[𝕜] M)