Stream: math-comp analysis

Topic: ✔ Lemma for differentiable -> derivable

view this post on Zulip abab9579 (Aug 30 2022 at 04:10):

apply/derivable1P/derivable1_diffP did the job, albeit I had to prove ( *:%R^~ v)is differentiable myself..

view this post on Zulip Notification Bot (Aug 30 2022 at 04:10):

abab9579 has marked this topic as resolved.

view this post on Zulip Cyril Cohen (Aug 30 2022 at 06:18):

Didn't differentiableZl do the job?

view this post on Zulip Cyril Cohen (Aug 30 2022 at 06:25):

Feel free to PR add the missing lemma to the library.

view this post on Zulip abab9579 (Aug 30 2022 at 08:29):

Oh, differentiableZl works. Dunno why I could not see it before.. Thank you!
By the way, can I know why is_diff_scalel is restricted to scaling R?

view this post on Zulip Cyril Cohen (Aug 30 2022 at 09:39):

abab9579 said:

Oh, differentiableZl works. Dunno why I could not see it before.. Thank you!
By the way, can I know why is_diff_scalel is restricted to scaling R?

I think it's a mistake and one can generalize for x : V.

view this post on Zulip Cyril Cohen (Aug 30 2022 at 09:44):

https://github.com/math-comp/analysis/pull/736

Last updated: Feb 05 2023 at 15:03 UTC