Skip to content

Commit 219be5b

Browse files
committed
chore: remove redundant simp attrs on forwardDiff_X and forwardDiff_C
1 parent a84f277 commit 219be5b

1 file changed

Lines changed: 0 additions & 2 deletions

File tree

Mathlib/RingTheory/HopfAlgebra/DeltaOperator.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -162,11 +162,9 @@ theorem forwardDiff_apply (a : R) (p : R[X]) :
162162
forwardDiff a p = taylor a p - p := by
163163
simp [forwardDiff]
164164

165-
@[simp]
166165
theorem forwardDiff_X (a : R) : forwardDiff a (X : R[X]) = C a := by
167166
simp [forwardDiff, taylor_X]
168167

169-
@[simp]
170168
theorem forwardDiff_C (a : R) (r : R) : forwardDiff a (C r) = 0 := by
171169
simp [forwardDiff, taylor_C]
172170

0 commit comments

Comments
 (0)