Holomorphy math-comp/analysis#204 · math-comp analysis

Stream: math-comp analysis

Topic: Holomorphy math-comp/analysis#204

Marie Kerjean (May 14 2020 at 11:25):

Has this PR been ported with respect to the commit porting closeness to Hausdorff spaces ? ?

Marie Kerjean (May 14 2020 at 11:26):

By the way, I'm renaming it holomorphy instead of cauchyetoile, if that's ok.

Marie Kerjean (May 14 2020 at 11:28):

I would like to commit the tentative description of derivability wrt R using within, if that's ok with you @Cyril Cohen @affeldt-aist ?

Reynald Affeldt (May 14 2020 at 11:38):

Yes, it has been rebased on top of the branch that brings the close predicate to Hausdorff space but the latter has since been merged into master.

Reynald Affeldt (May 14 2020 at 12:02):

I just did a rebase of PR 192 on top of master (with a small update).

Marie Kerjean (May 14 2020 at 12:40):

Which fork/branch of real-closed should this PR depends on ? I have my fork of @Kazuhiko Sakaguchi own fork, where I have deleted the canonical R-vector space structure on C , but this has been implemented elsewhere maybe ?

Cyril Cohen (May 14 2020 at 14:11):

@mkerjean I was waiting for your opinion before merging math-comp/real-closed#23

Cyril Cohen (May 14 2020 at 14:12):

Then I will release and you/we can use a released version in math-comp/analysis

Reynald Affeldt (May 14 2020 at 14:15):

(CI fails for PR#204, even though it compiles on my computer and PR#192 was fine)

Marie Kerjean (May 14 2020 at 14:21):

I'm sorry I missed this PR (if I don't answer within 2 days you can ping me again). I think it's enough, but I'll be able to test it tomorrow if you can wait.