Mathlib has a bunch of internal structure. For example:
import Mathlib.Algebra.*
import Mathlib.AlgebraicGeometry.AffineScheme
import Mathlib.AlgebraicGeometry.AffineSpace
import Mathlib.AlgebraicGeometry.Cover.*
import Mathlib.AlgebraicGeometry.EllipticCurve.Affine
import Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.*
import Mathlib.AlgebraicGeometry.EllipticCurve.Group
import Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
import Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.*
import Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
import Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
import Mathlib.AlgebraicGeometry.EllipticCurve.Projective.*
import Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
import Mathlib.AlgebraicGeometry.Fiber
[..]
We should decide on a similar structure for Cryptolib. We can obviously adjust it over time as we figure out more about the internal structure, but we should try and start from a place of organization.
Mathlib has a bunch of internal structure. For example:
We should decide on a similar structure for Cryptolib. We can obviously adjust it over time as we figure out more about the internal structure, but we should try and start from a place of organization.