Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Holomorphy #192

Closed
wants to merge 11 commits into from
Closed

Holomorphy #192

wants to merge 11 commits into from

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Apr 29, 2020 •
edited
Loading

This PR gathers commits that contribute to cauchyetoile.v by @mkerjean. They were cherry-picked from the branch mathcomp_master_integral_ereal. Some are the results of splits of commits from mathcomp_master_integral_ereal.

@affeldt-aist affeldt-aist marked this pull request as draft April 29, 2020 17:06
@CohenCyril CohenCyril force-pushed the mathcomp_master_hausdorff_close branch from 4f1de13 to 17086dc Compare May 4, 2020 15:31
@CohenCyril CohenCyril force-pushed the cauchy_etoile branch 2 times, most recently from 106d4f8 to d26c2ae Compare May 4, 2020 15:56
@mkerjean
Copy link
Collaborator

mkerjean commented May 4, 2020 •
edited by CohenCyril
Loading

You've been updating complex with respect to PR#270 ? For information I tested another formalism for the real structure on C (basically, nothing of the previous Rcomplex is canonical anymore), and I used within R to speak about real differentiation. Here it is : https://github.com/mkerjean/analysis/blob/mathcomp_master_topologicalring/theories/holomorphy.v.
It does shorten the proofs. In another branch I tried to take out the R^o notation to ease the proof of CauhyRiemann -> holomorphic.

@CohenCyril
Copy link
Member

You've been updating complex with respect to PR#270 ?

Yes, complex has been updated wrt mathcomp 1.11.0+beta1 ... Apparently, I forgot to withdraw the module structure, though :-/

@CohenCyril
Copy link
Member

and I used within R to speak about real differentiation.

I think that's really nice :)

@CohenCyril CohenCyril force-pushed the mathcomp_master_hausdorff_close branch from 17086dc to 7d1689b Compare May 6, 2020 18:26
@mkerjean mkerjean changed the title Cauchy etoile Holomorphy May 14, 2020
@affeldt-aist affeldt-aist changed the base branch from mathcomp_master_hausdorff_close to master May 14, 2020 12:00
@mkerjean mkerjean closed this May 14, 2020
@mkerjean mkerjean deleted the cauchy_etoile branch May 14, 2020 13:24
@mkerjean mkerjean mentioned this pull request May 15, 2020
Draft
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@affeldt-aist @mkerjean @CohenCyril