Paper XII · Lean sources

Patching Support, Hecke Packets, and Conditional Automorphic Completion

Inherited / related evidence Coverage and evidence

The edition relies on earlier or related formal evidence. That evidence is not a fresh full-edition replay.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

Edit and run in your browser

Source files 96

Source locations and editions

Files are shown relative to core/publication/source/lean_guide/formal_release/lean/.

Historical editions keep their original paths. Package caches and build files are omitted.

96 files

ClassInvariants.leanPaperX/
103 lines · 15 declaration locations
Reconstruction.leanPaperX/
189 lines · 19 declaration locations
RepresentationClasses.leanPaperX/
132 lines · 24 declaration locations
RepresentationLimits.leanPaperX/
193 lines · 28 declaration locations
RepresentationTopology.leanPaperX/
124 lines · 11 declaration locations
AdicCompanions.leanPaperXII/
134 lines · 14 declaration locations
AdicCompletionComparison.leanPaperXII/
210 lines · 19 declaration locations
AdicLocalConditions.leanPaperXII/
116 lines · 11 declaration locations
AdicMatrixGroups.leanPaperXII/
163 lines · 22 declaration locations
AdicModel.leanPaperXII/
73 lines · 15 declaration locations
AdicQuotientTopology.leanPaperXII/
105 lines · 13 declaration locations
AdicSpines.leanPaperXII/
112 lines · 7 declaration locations
ArtinData.leanPaperXII/
97 lines · 11 declaration locations
ArtinModules.leanPaperXII/
206 lines · 23 declaration locations
AugmentationCoinvariants.leanPaperXII/
120 lines · 15 declaration locations
AuxiliaryGroupAlgebra.leanPaperXII/
72 lines · 11 declaration locations
BalancedAugmentation.leanPaperXII/
128 lines · 17 declaration locations
BaseChangeSupport.leanPaperXII/
47 lines · 4 declaration locations
ClassCompanions.leanPaperXII/
197 lines · 18 declaration locations
ClassSpines.leanPaperXII/
116 lines · 4 declaration locations
CoinvariantTensorComparison.leanPaperXII/
108 lines · 9 declaration locations
Coinvariants.leanPaperXII/
47 lines · 2 declaration locations
CompanionForests.leanPaperXII/
84 lines · 11 declaration locations
CompletedBaseChangeTransport.leanPaperXII/
113 lines · 12 declaration locations
CompletedFiniteTensor.leanPaperXII/
134 lines · 15 declaration locations
CompletedGlobalBaseChange.leanPaperXII/
263 lines · 26 declaration locations
CompletedGlobalQuotient.leanPaperXII/
173 lines · 22 declaration locations
CompletedLocalConditions.leanPaperXII/
100 lines · 11 declaration locations
CompletedPaperCapstone.leanPaperXII/
69 lines · 3 declaration locations
CompletedPointCategory.leanPaperXII/
101 lines · 7 declaration locations
CompletedTensorUniversal.leanPaperXII/
99 lines · 8 declaration locations
CompletionBoundaryChecks.leanPaperXII/
45 lines · 4 declaration locations
CompletionQuotient.leanPaperXII/
181 lines · 30 declaration locations
ComplexBaseChange.leanPaperXII/
86 lines · 11 declaration locations
ComplexFieldFibers.leanPaperXII/
108 lines · 9 declaration locations
ComplexSupport.leanPaperXII/
103 lines · 11 declaration locations
ComponentSupport.leanPaperXII/
21 lines · 1 declaration location
ConditionalCompletion.leanPaperXII/
54 lines · 1 declaration location
ContinuousClasses.leanPaperXII/
112 lines · 13 declaration locations
CorrectedOccupancy.leanPaperXII/
24 lines · 1 declaration location
DenseFrobenius.leanPaperXII/
113 lines · 9 declaration locations
DerivedHeckeAction.leanPaperXII/
116 lines · 11 declaration locations
DerivedPatching.leanPaperXII/
92 lines · 11 declaration locations
DerivedRealization.leanPaperXII/
177 lines · 8 declaration locations
DeterminantalBlockStabilization.leanPaperXII/
83 lines · 10 declaration locations
DeterminantalIdeals.leanPaperXII/
131 lines · 12 declaration locations
DeterminantalStabilization.leanPaperXII/
130 lines · 13 declaration locations
DyadicProjectors.leanPaperXII/
195 lines · 26 declaration locations
DyadicProjectorsResidual.leanPaperXII/
124 lines · 21 declaration locations
ExistingCompatibleSystems.leanPaperXII/
81 lines · 3 declaration locations
FieldFibers.leanPaperXII/
73 lines · 8 declaration locations
FiniteAdequacy.leanPaperXII/
109 lines · 9 declaration locations
FiniteCarrier.leanPaperXII/
67 lines · 7 declaration locations
FiniteGroupCohomology.leanPaperXII/
107 lines · 10 declaration locations
FiniteTensorLocality.leanPaperXII/
149 lines · 15 declaration locations
FiniteTensorQuotient.leanPaperXII/
172 lines · 25 declaration locations
FittingBaseChange.leanPaperXII/
60 lines · 4 declaration locations
FittingBoundaryChecks.leanPaperXII/
66 lines · 6 declaration locations
FittingStrata.leanPaperXII/
64 lines · 5 declaration locations
FittingTransport.leanPaperXII/
60 lines · 4 declaration locations
FiveGateCompletion.leanPaperXII/
168 lines · 7 declaration locations
FrobeniusSeparation.leanPaperXII/
76 lines · 10 declaration locations
GaloisRealization.leanPaperXII/
98 lines · 7 declaration locations
GeneralizedPackets.leanPaperXII/
137 lines · 7 declaration locations
HeckeCarriers.leanPaperXII/
237 lines · 29 declaration locations
HeckeFibers.leanPaperXII/
90 lines · 9 declaration locations
IntrinsicFitting.leanPaperXII/
69 lines · 8 declaration locations
InverseLimitRepresentations.leanPaperXII/
169 lines · 17 declaration locations
LocalIdempotents.leanPaperXII/
18 lines · 1 declaration location
LocalQuotients.leanPaperXII/
126 lines · 14 declaration locations
ModuleSupport.leanPaperXII/
63 lines · 10 declaration locations
NonabelianResidual.leanPaperXII/
142 lines · 10 declaration locations
OrdinaryCompletion.leanPaperXII/
213 lines · 9 declaration locations
OrdinaryPatching.leanPaperXII/
98 lines · 5 declaration locations
PacketTrace.leanPaperXII/
74 lines · 10 declaration locations
PatchingCarriers.leanPaperXII/
109 lines · 12 declaration locations
PerfectCohomology.leanPaperXII/
108 lines · 12 declaration locations
PerfectDerivedSupport.leanPaperXII/
119 lines · 17 declaration locations
PerfectModels.leanPaperXII/
122 lines · 10 declaration locations
PowerSeriesComponent.leanPaperXII/
246 lines · 56 declaration locations
PresentationComparison.leanPaperXII/
122 lines · 7 declaration locations
PresentationIndependence.leanPaperXII/
63 lines · 2 declaration locations
QuotientSupport.leanPaperXII/
60 lines · 5 declaration locations
RepresentationData.leanPaperXII/
86 lines · 11 declaration locations
ResidualAugmentation.leanPaperXII/
78 lines · 6 declaration locations
ReuseCompactness.leanPaperXII/
175 lines · 19 declaration locations
ReuseFiniteSeparation.leanPaperXII/
97 lines · 8 declaration locations
RightAugmentation.leanPaperXII/
91 lines · 10 declaration locations
S3Adjoint.leanPaperXII/
240 lines · 34 declaration locations
S3Detection.leanPaperXII/
316 lines · 33 declaration locations
S3Spectrum.leanPaperXII/
86 lines · 9 declaration locations
S3Standard.leanPaperXII/
221 lines · 36 declaration locations
StableCores.leanPaperXII/
92 lines · 10 declaration locations
SupportTransport.leanPaperXII/
59 lines · 4 declaration locations
TruncatedGroupAlgebra.leanPaperXII/
297 lines · 37 declaration locations
VectorInverseLimit.leanPaperXII/
122 lines · 14 declaration locations