Documentation

GQ2.Foundations

Classical foundations #

The literature axioms (B1, B5, B7, B7′, …) now live in GQ2/Foundations/Axioms.lean — the single file allowed to contain axiom declarations (enforced by scripts/check_axioms.sh). This module remains as a re-export so import GQ2.Foundations keeps working; all names are unchanged (GQ2.Foundations.absGalQ2_isTopologicallyFinitelyGenerated, …).