fix theorem name

lecopivo · Nov 18, 2024 · 5ea2973 · 5ea2973
1 parent 7f5890f
commit 5ea2973
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/SciLean/Analysis/Calculus/Monad/StateT.lean b/SciLean/Analysis/Calculus/Monad/StateT.lean
@@ -193,8 +193,10 @@ variable
   [LawfulMonad m] [LawfulMonad m']
 
 @[simp]
-theorem add_zero {α} [AddGroup α] : (HAdd.hAdd 0 : α → α) = fun x => x := by funext x; simp
+theorem add_zero_left {α} [AddZeroClass α] :
+  (HAdd.hAdd 0 : α → α) = fun x => x := by funext x; simp
 
+open RevFDerivMonad in
 noncomputable
 instance (S : Type) [NormedAddCommGroup S] [AdjointSpace K S] [CompleteSpace S] :
     RevFDerivMonad K (StateT S m) (StateT S m') where