From e2f0924489e6b36baa14779b36b9d9230fc337c5 Mon Sep 17 00:00:00 2001
From: Shing Tak Lam <shingtaklam1324@gmail.com>
Date: Sun, 4 Sep 2022 07:59:51 +0100
Subject: [PATCH] Update src/analysis/inner_product_space/adjoint.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
---
 src/analysis/inner_product_space/adjoint.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analysis/inner_product_space/adjoint.lean b/src/analysis/inner_product_space/adjoint.lean
index cbad153ea6f6f..88dba7d047011 100644
--- a/src/analysis/inner_product_space/adjoint.lean
+++ b/src/analysis/inner_product_space/adjoint.lean
@@ -103,7 +103,7 @@ linear_isometry_equiv.of_surjective
 
 localized "postfix (name := adjoint) `†`:1000 := continuous_linear_map.adjoint" in inner_product
 
-@[simp] lemma adjoint_apply (A : E →L[𝕜] F) (x : F) :
+lemma adjoint_apply (A : E →L[𝕜] F) (x : F) :
   A† x = ((to_dual 𝕜 E).symm : (normed_space.dual 𝕜 E) → E) ((to_sesq_form A) x) := rfl
 
 /-- The fundamental property of the adjoint. -/