define AdjointSpace that provides inner product without restricting norm

lecopivo · Jun 21, 2024 · 96e3070 · 96e3070
1 parent 9bfa80c
commit 96e3070
Show file tree

Hide file tree

Showing 4 changed files with 908 additions and 0 deletions.
diff --git a/SciLean/Core/Simp.lean b/SciLean/Core/Simp.lean
@@ -10,3 +10,6 @@ register_simp_attr neg_pull
 register_simp_attr neg_push
 register_simp_attr smul_pull
 register_simp_attr smul_push
+
+
+register_simp_attr simp_core