Update src/analysis/inner_product_space/adjoint.lean

Co-authored-by: Frédéric Dupuis <[email protected]>
leanprover-community · Sep 4, 2022 · e2f0924 · e2f0924
1 parent c32d8e4
commit e2f0924
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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. -/