The complete development
Lean source browser
All 73 mathematical modules, the aggregate import, and the audit. Each page contains the exact source with numbered lines and a raw download.
Core and supporting modules
- Analysis.lean
- BallOrderGeometry.lean
- BallScaling.lean
- BooleanGap.lean
- BoundedFamilies.lean
- C0Profiles.lean
- Center.lean
- CenteredSynthesis.lean
- ChainCompleteness.lean
- Characterization.lean
- ClopenCompleteness.lean
- ClopenPairs.lean
- CofinalReindexing.lean
- CofinalSequences.lean
- ComplexBall.lean
- ContinuousBall.lean
- ConvexIntegral.lean
- CountablePairs.lean
- Cozero.lean
- Deficits.lean
- DelayPrefixBound.lean
- DiscretePropagation.lean
- EDSupremum.lean
- EncodedDomain.lean
- EncodedMaps.lean
- EncodedRecurrence.lean
- EncodedRules.lean
- EnvelopeOrder.lean
- Envelopes.lean
- ExtensionDelay.lean
- Families.lean
- FiniteSynthesis.lean
- FSpaceNecessary.lean
- Hartogs.lean
- IndexedGaps.lean
- Interleaving.lean
- InterleavingEnvelopes.lean
- InvariantIntervals.lean
- LatticeFixedPoint.lean
- MainTransfinite.lean
- Necessity.lean
- OrdinalCofinality.lean
- OrdinalIndex.lean
- OrdinalPairs.lean
- PositiveSynthesis.lean
- PrefixFactorization.lean
- ProfileExtension.lean
- ProfileGeometry.lean
- ProfileRestriction.lean
- Profiles.lean
- Realization.lean
- Regularization.lean
- RegularPairs.lean
- SaturatedChains.lean
- SignExtension.lean
- SignRealization.lean
- SignRecursion.lean
- SignTermination.lean
- StepAlgebra.lean
- StepFunctions.lean
- Suprema.lean
- SynthesisIntegral.lean
- SynthesisMeasure.lean
- Transfer.lean
- TransfinitePropagator.lean
- TwoProfileGeometry.lean
- TwoProfiles.lean
- TwoProfileStructure.lean