rm Module.endUnitsToModuleAutEquiv

leanprover-community · Oct 30, 2024 · 2f2440b · 2f2440b
1 parent e8d24de
commit 2f2440b
Showing 1 changed file with 0 additions and 13 deletions.
diff --git a/Mathlib/Algebra/Module/Equiv/Basic.lean b/Mathlib/Algebra/Module/Equiv/Basic.lean
@@ -196,19 +196,6 @@ def toModuleAut : S →* M ≃ₗ[R] M where
 
 end DistribMulAction
 
-/-- An isomorphism from invertible linear endomorphisms to linear automorphisms. -/
-def Module.endUnitsToModuleAutEquiv (R) (M) [CommRing R] [AddCommGroup M] [Module R M] :
-    (M →ₗ[R] M)ˣ ≃* (M ≃ₗ[R] M) where
-  toFun f := DistribMulAction.toLinearEquiv R M f
-  invFun f := ⟨f, f.symm, by ext; simp, by ext; simp⟩
-  left_inv f := by ext; simp [Units.smul_def]
-  right_inv f := by ext; simp
-  map_mul' f g := by
-    ext x
-    simp only [DistribMulAction.toLinearEquiv_apply, mul_smul,
-      show (DistribMulAction.toLinearEquiv R M f * DistribMulAction.toLinearEquiv R M g) x =
-      DistribMulAction.toLinearEquiv R M f ((DistribMulAction.toLinearEquiv R M g) x) by rfl]
-
 namespace AddEquiv
 
 section AddCommMonoid