Skip to content

Commit 41a8000

Browse files
committed
rm blank line
1 parent c6c14b0 commit 41a8000

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

theories/derive.v

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -552,7 +552,6 @@ Proof. by apply/diff_unique; have [] := dcst a x. Qed.
552552

553553
Variables (V W : normedModType R).
554554

555-
556555
Lemma differentiable_cst (W' : normedModType R) (a : W') (x : V) :
557556
differentiable (cst a) x.
558557
Proof. by apply/diff_locallyP; rewrite diff_cst; have := dcst a x. Qed.

0 commit comments

Comments
 (0)