OAI/AlgebraicGeometry/CharacterVarieties.lean

GitHub source file

0 declarations, 0 contain sorry, 0 declared as axioms

Marked nonseparating cuts of surface diagrams

This development formalizes the surface diagrams, framed flag equations, and construction of solutions under a marked nonseparating cut from Integral points on character varieties of curves by OpenAI.

This file declares nothing itself. It gathers the 5 imports below, so a file that imports it gets all of them.

Imports

Imported by 1 file