I tried looking around the web for this and via GitHub code search but didn't find anything. Is there a formalization of smooth manifolds in Coq? I would be fine with using a classical construction. There seems to be some papers on a formalization using Isabelle/HOL light, but none in Coq.
Last updated: Oct 05 2023 at 02:01 UTC