-- The Cumulus mathematics library
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus
import Real
import Rat
import Cardinal
import Order
import Ordinal
import Set.MaximalPrinciple
import Set.WellOrdering
import Cardinal.Infinite
import Cardinal.Algebra
import Cardinal.Square
import Cardinal.Combinations
import List
import Topology
import FixedPoint
import Algebra.Ring.MaximalIdeal
import NumberTheory
import Algebra
import LinearAlgebra
import GraphTheory
-- The friendship theorem's modules reach the choice axiom only through the
-- Combinatorics area's imports, so they join the library here rather than
-- in the GraphTheory root, which stays available under ZF.
import GraphTheory.Friendship
-- The cycle double cover theorem chooses base sums and cycle decompositions
-- through Set.Choice, so its last modules join the library here rather than
-- in the GraphTheory root, which stays available under ZF.
import GraphTheory.DoubleCover.Theorem
import GameTheory
import Geometry
-- The absorption layer of the Banach–Tarski development uses the choice
-- axiom through Set.Choice, so it joins the library here rather than in
-- the Geometry root, which stays available under ZF.
import Geometry.Absorption
import Complex
import Complex.Nullstellensatz
import Complex.Cubic
import Complex.Quartic
import Complex.FundamentalTheoremGeneral
import Lattice
import Combinatorics
import Category
import Probability
import Metric
import Rotation
import Geometry.Hausdorff
import Geometry.Sphere
import Geometry.BanachTarski
import Geometry.BanachTarski.Strong

-- GRACE17 Cumulus: reusable, kernel-checked mathematics over sets.