Update Mathlib/Topology/Algebra/Module/Basic.lean

Co-authored-by: Eric Wieser <[email protected]>
leanprover-community · Oct 15, 2024 · 533b2be · 533b2be
1 parent 88d1ec6
commit 533b2be
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean
@@ -2407,6 +2407,7 @@ variable (R : Type*) [Semiring R] [τR : TopologicalSpace R] [TopologicalSemirin
   {M : Type*} [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousSMul R M]
 
 /-- The function `op` is a continuous linear equivalence. -/
+@[simps!]
 def opContinuousLinearEquiv : M ≃L[R] Mᵐᵒᵖ where
   __ := MulOpposite.opLinearEquiv R