chore(linear_algebra/basic): golf linear_equiv.smul_of_unit (#12190)

This already exists more generally as `distrib_mul_action.to_linear_equiv`.

The name is probably more discoverable and it needs fewer arguments, so I've left it around for now.

src/linear_algebra/basic.lean

@@ -2378,9 +2378,7 @@ open _root_.linear_map
 
 /-- Multiplying by a unit `a` of the ring `R` is a linear equivalence. -/
 def smul_of_unit (a : Rˣ) : M ≃ₗ[R] M :=
-of_linear ((a:R) • 1 : M →ₗ[R] M) (((a⁻¹ : Rˣ) : R) • 1 : M →ₗ[R] M)
-  (by rw [smul_comp, comp_smul, smul_smul, units.mul_inv, one_smul]; refl)
-  (by rw [smul_comp, comp_smul, smul_smul, units.inv_mul, one_smul]; refl)
+distrib_mul_action.to_linear_equiv R M a
 
 /-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives a
 linear isomorphism between the two function spaces. -/

src/linear_algebra/finite_dimensional.lean

@@ -596,7 +596,8 @@ b.map (linear_equiv.smul_of_unit (units.mk0
   basis_singleton ι h v hv i = v :=
 calc basis_singleton ι h v hv i
     = (((basis_unique ι h).repr) v) default • (basis_unique ι h) default :
-      by simp [subsingleton.elim i default, basis_singleton, linear_equiv.smul_of_unit]
+      by simp [subsingleton.elim i default, basis_singleton, linear_equiv.smul_of_unit,
+               units.smul_def]
 ... = v : by rw [← finsupp.total_unique K (basis.repr _ v), basis.total_repr]
 
 @[simp] lemma range_basis_singleton (ι : Type*) [unique ι]