coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Differential Geometry Module Proposal

From: Li-yao Xia <lysxia AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Differential Geometry Module Proposal
Date: Thu, 9 Aug 2018 15:52:00 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lysxia AT gmail.com; spf=Pass smtp.mailfrom=lysxia AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f47.google.com
Ironport-phdr: 9a23:G6h6/xzmk6qPjirXCy+O+j09IxM/srCxBDY+r6Qd1eMTIJqq85mqBkHD//Il1AaPAd2Fraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HSbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRH1likHOT43/mLZhMN+g61Uog6uqRNkzo7IYoyYLuZycr/TcN4YQ2dKQ8ZfVzZGAoO5d4YBCesBMf9YrobnoFsFsBqxBQi2C+jyzTJIgn/33bY10uQgCw7LxwMgH9cUv3TVqNX5LrsdUeewzKTRyzjIcvBY2S/l5YTWbhwspeuAULFwfMbL10UjCR7Jgk+fpIHnJz+Y1foBv3Ka4udvT+6ihGEqpxtwrzWgwMonl5PHiZgPyl/e8CV02IY1KsO8SE58edOkFYFftyCeN4dvTMIiWXxktD80yrAJu5O3ZicKyJMgxx7Qb/yIbZKE7Q7kVOaUOTt4hXRld6yjhxuq70Ss1unxWtO33VtKtCZJjMfAum0X2xHc6MWLUv598V2g2TaL2QDT8OZEIUUsmKrfK58h2bExlpsJvknYES/2nV/5jK6Sdkk+5ueo7OHnbq38ppCAL490lh3+MqM2l8OjBuQ4KxECUHSf+eShz7Lu5lb5QbVPjv0uiKbVqpHaJcIBpq64GQBZyIgj6wzsRwuhhd8fhDwMKE9PUBOBlYngfV/Uc97iCvLqp1XpgT5sj8DHN/W1BoTWPnnKuLjkdLd5rUVbzVxgnphk+5tIB+RZc7rIUUjruYmAV05rA0mP2+/iTe5F+MYbUGOLDLWeNfqL41CN7+MrZeKLYd1M4WqvG70e//fryEQBtxoFZ6DwhMkYbXm5GrJtJEDLOSOx0OdEKn8Du08FdMKviFCGVmQONXO7XqZ5+StiTYz6UsHMQYeihLHH1yC+TMVb

I wonder whether synthetic differential geometry would be an interesting starting point for such a project.

Li-yao

On 08/09/2018 02:30 PM, Larry Lee wrote:

Hi,

I'm looking for mathematical fields that currently do not have any contributed developments and noticed that none of the modules listed in the Coq Package Index appeared to cover differential geometry. I'd like to develop a module covering basic results, but I'd like to avoid duplicating existing work. Does anyone know of any Coq modules that cover Differential Geometry? If not, would anyone like to share any recommendations/requests concerning the new module?

Thanks,
- Larry Lee

[Coq-Club] Differential Geometry Module Proposal, Larry Lee, 08/09/2018
- Re: [Coq-Club] Differential Geometry Module Proposal, Li-yao Xia, 08/09/2018
- Re: [Coq-Club] Differential Geometry Module Proposal, Thomas Burdick, 08/13/2018