Paper XI · Lean sources

Packets, Arithmetic Realization, and Conditional Comparison

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

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

Edit and run in your browser

Source files 430

Source locations and editions

Files are shown relative to formalization/.

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

430 files

PaperXI.lean
423 lines · 0 declaration locations
AbstractHeisenberg.leanPaperXI/
184 lines · 35 declaration locations
AbstractHeisenbergExtension.leanPaperXI/
58 lines · 5 declaration locations
ActualCartanCandidate106.leanPaperXI/
79 lines · 1 declaration location
ActualCharacterCandidate108.leanPaperXI/
89 lines · 1 declaration location
ActualCharacterData108.leanPaperXI/
49 lines · 5 declaration locations
ActualCharacterIdentification61.leanPaperXI/
100 lines · 3 declaration locations
ActualCharacterResidue61.leanPaperXI/
133 lines · 7 declaration locations
ActualCharacterType61.leanPaperXI/
163 lines · 14 declaration locations
ActualCompactTypeCompletion58.leanPaperXI/
97 lines · 2 declaration locations
ActualCoordinateDeepIdeal111.leanPaperXI/
80 lines · 6 declaration locations
ActualCuspidalCandidate105.leanPaperXI/
118 lines · 5 declaration locations
ActualDepthZeroExtension.leanPaperXI/
155 lines · 21 declaration locations
ActualELatticeFieldJoin59.leanPaperXI/
80 lines · 5 declaration locations
ActualELatticeFreeness59.leanPaperXI/
73 lines · 6 declaration locations
ActualELatticeNormalizer59.leanPaperXI/
129 lines · 7 declaration locations
ActualELatticeQuotient59.leanPaperXI/
89 lines · 12 declaration locations
ActualELatticeResidue59.leanPaperXI/
157 lines · 19 declaration locations
ActualELatticeScalarPeriod60.leanPaperXI/
87 lines · 4 declaration locations
ActualELatticeTopology60.leanPaperXI/
170 lines · 16 declaration locations
ActualELatticeTypeGroup59.leanPaperXI/
136 lines · 13 declaration locations
ActualEmbeddedUniformizer58.leanPaperXI/
177 lines · 13 declaration locations
ActualFieldTypeQuotient69.leanPaperXI/
157 lines · 8 declaration locations
ActualGroupIndex111.leanPaperXI/
273 lines · 9 declaration locations
ActualHeisenbergCandidate107.leanPaperXI/
89 lines · 1 declaration location
ActualIntegerTower111.leanPaperXI/
178 lines · 16 declaration locations
ActualIntegralGeneralLinear.leanPaperXI/
219 lines · 27 declaration locations
ActualIntersection108.leanPaperXI/
59 lines · 5 declaration locations
ActualLocalCartan106.leanPaperXI/
44 lines · 3 declaration locations
ActualLocalUnitDecomposition.leanPaperXI/
128 lines · 20 declaration locations
ActualLocalUnitTopology.leanPaperXI/
102 lines · 13 declaration locations
ActualMonomialLocalGlobal.leanPaperXI/
507 lines · 35 declaration locations
ActualNormalizerTypeExtension58.leanPaperXI/
82 lines · 2 declaration locations
ActualOnePlusTopology111.leanPaperXI/
114 lines · 5 declaration locations
ActualPacketTypeRealization70.leanPaperXI/
109 lines · 1 declaration location
ActualProfileCandidate110.leanPaperXI/
94 lines · 1 declaration location
ActualResidueGeneralLinear.leanPaperXI/
69 lines · 7 declaration locations
ActualScalarLift113.leanPaperXI/
221 lines · 15 declaration locations
ActualSourceCandidate111.leanPaperXI/
102 lines · 1 declaration location
ActualUnramifiedBaseChange.leanPaperXI/
115 lines · 8 declaration locations
AlgebraActionModule.leanPaperXI/
250 lines · 42 declaration locations
ArithmeticAttachment110.leanPaperXI/
161 lines · 7 declaration locations
ArithmeticFieldInduction69.leanPaperXI/
83 lines · 5 declaration locations
ArithmeticTypeCertificate69.leanPaperXI/
106 lines · 6 declaration locations
AtomicMultiset.leanPaperXI/
122 lines · 20 declaration locations
AtomicNaturality.leanPaperXI/
106 lines · 7 declaration locations
AtomicReconstruction.leanPaperXI/
153 lines · 20 declaration locations
BilinearHeisenberg.leanPaperXI/
152 lines · 25 declaration locations
BoundaryExamples.leanPaperXI/
30 lines · 6 declaration locations
BreakBridge.leanPaperXI/
104 lines · 5 declaration locations
BreakBridgeAlong.leanPaperXI/
80 lines · 2 declaration locations
BreakDyadicPhase.leanPaperXI/
115 lines · 8 declaration locations
BreakHeisenbergSum.leanPaperXI/
143 lines · 18 declaration locations
BreakMoving.leanPaperXI/
116 lines · 10 declaration locations
BreakOddPhase.leanPaperXI/
164 lines · 10 declaration locations
BreakQuadratic.leanPaperXI/
104 lines · 11 declaration locations
BreakTensorFactorization.leanPaperXI/
77 lines · 2 declaration locations
BreakTensorMap.leanPaperXI/
100 lines · 11 declaration locations
CanonicalDVRValuation.leanPaperXI/
225 lines · 27 declaration locations
CentralCharacterAction.leanPaperXI/
111 lines · 9 declaration locations
CentralCharacterInduction.leanPaperXI/
62 lines · 3 declaration locations
CentralCharacterIrreducible.leanPaperXI/
49 lines · 3 declaration locations
CentralCharacterRepresentation.leanPaperXI/
83 lines · 8 declaration locations
CentralExtension.leanPaperXI/
85 lines · 14 declaration locations
CentralExtensionCocycle.leanPaperXI/
127 lines · 19 declaration locations
CentralExtensionComparison.leanPaperXI/
61 lines · 3 declaration locations
CentralExtensionExistence.leanPaperXI/
43 lines · 1 declaration location
CentralExtensionInducing.leanPaperXI/
208 lines · 20 declaration locations
CentralExtensionInductionConsequences.leanPaperXI/
95 lines · 6 declaration locations
CentralExtensionSectionChange.leanPaperXI/
267 lines · 27 declaration locations
CentralExtensionStructure.leanPaperXI/
117 lines · 11 declaration locations
CentralExtensionUniqueness.leanPaperXI/
99 lines · 6 declaration locations
CentralProduct.leanPaperXI/
159 lines · 27 declaration locations
CentralProductCommutator.leanPaperXI/
72 lines · 4 declaration locations
CentralProductComparison.leanPaperXI/
149 lines · 17 declaration locations
CentralProductFactors.leanPaperXI/
89 lines · 9 declaration locations
CentralProductMap.leanPaperXI/
64 lines · 7 declaration locations
ChainSharpness.leanPaperXI/
25 lines · 2 declaration locations
CharacterAttachment108.leanPaperXI/
73 lines · 4 declaration locations
CharacterGenerators.leanPaperXI/
59 lines · 4 declaration locations
CharacterNormalizer61.leanPaperXI/
104 lines · 10 declaration locations
CharacterPairing108.leanPaperXI/
78 lines · 2 declaration locations
CharacterProjector.leanPaperXI/
100 lines · 8 declaration locations
CharacterSupport108.leanPaperXI/
71 lines · 6 declaration locations
CharacterTwist.leanPaperXI/
54 lines · 7 declaration locations
CliffordAction.leanPaperXI/
86 lines · 2 declaration locations
CliffordChoices.leanPaperXI/
148 lines · 12 declaration locations
CliffordCocycle.leanPaperXI/
98 lines · 8 declaration locations
CliffordCocycleChoices.leanPaperXI/
87 lines · 7 declaration locations
CliffordCocycleClass.leanPaperXI/
111 lines · 8 declaration locations
CliffordDatum.leanPaperXI/
112 lines · 20 declaration locations
CliffordEnvelope.leanPaperXI/
147 lines · 16 declaration locations
CliffordEvaluation.leanPaperXI/
242 lines · 22 declaration locations
CliffordHeisenbergAttachment.leanPaperXI/
144 lines · 8 declaration locations
CliffordIrreducible.leanPaperXI/
98 lines · 8 declaration locations
CliffordMultiplicity.leanPaperXI/
241 lines · 24 declaration locations
CliffordPacket.leanPaperXI/
68 lines · 7 declaration locations
CliffordSource.leanPaperXI/
48 lines · 4 declaration locations
CliffordStabilizer.leanPaperXI/
216 lines · 14 declaration locations
CliffordTransport.leanPaperXI/
280 lines · 27 declaration locations
CocycleBasis.leanPaperXI/
33 lines · 2 declaration locations
CocycleClass.leanPaperXI/
168 lines · 24 declaration locations
CocycleCommutator.leanPaperXI/
122 lines · 18 declaration locations
CocycleQuotient.leanPaperXI/
85 lines · 10 declaration locations
CommutatorEnvelope.leanPaperXI/
160 lines · 16 declaration locations
CompactDegreeSeparation.leanPaperXI/
37 lines · 2 declaration locations
CompactIntersection108.leanPaperXI/
55 lines · 4 declaration locations
CompactModCenterInduction68.leanPaperXI/
126 lines · 4 declaration locations
CompactQuotientPeriod69.leanPaperXI/
52 lines · 1 declaration location
CompactSmoothSemisimple.leanPaperXI/
92 lines · 8 declaration locations
CompactTypeTensor58.leanPaperXI/
93 lines · 7 declaration locations
CompactTypeTensorNormalizer58.leanPaperXI/
54 lines · 5 declaration locations
ConditionalAtomicComparison.leanPaperXI/
151 lines · 14 declaration locations
ConstructedFieldFrobenius.leanPaperXI/
65 lines · 6 declaration locations
ContinuousHolonomyResidual.leanPaperXI/
132 lines · 12 declaration locations
CoordinateDeepIdeal111.leanPaperXI/
79 lines · 4 declaration locations
CuspidalAnnihilation.leanPaperXI/
87 lines · 10 declaration locations
CuspidalCartan105.leanPaperXI/
82 lines · 4 declaration locations
CuspidalContraction105.leanPaperXI/
37 lines · 4 declaration locations
CycleCoordinates.leanPaperXI/
97 lines · 9 declaration locations
CycleFixed.leanPaperXI/
138 lines · 9 declaration locations
CycleSpan.leanPaperXI/
76 lines · 11 declaration locations
CyclicAction.leanPaperXI/
55 lines · 9 declaration locations
CyclicBridge.leanPaperXI/
111 lines · 8 declaration locations
CyclicDefect113.leanPaperXI/
339 lines · 37 declaration locations
CyclicFrobeniusCount.leanPaperXI/
120 lines · 12 declaration locations
CyclicInducedBasis.leanPaperXI/
83 lines · 12 declaration locations
CyclicInducedCharacter.leanPaperXI/
60 lines · 6 declaration locations
CyclicInducedCoordinates.leanPaperXI/
179 lines · 25 declaration locations
CyclicInducedDegree.leanPaperXI/
59 lines · 10 declaration locations
CyclicInducedWrap.leanPaperXI/
119 lines · 12 declaration locations
CyclicLinearization.leanPaperXI/
83 lines · 5 declaration locations
CyclicNormalization113.leanPaperXI/
386 lines · 22 declaration locations
CyclicPolynomial.leanPaperXI/
81 lines · 7 declaration locations
DVRCartan106.leanPaperXI/
68 lines · 3 declaration locations
DegreeIndex110.leanPaperXI/
432 lines · 19 declaration locations
DerivedCentralCharacter69.leanPaperXI/
41 lines · 4 declaration locations
DiscrepancyCharacter.leanPaperXI/
50 lines · 1 declaration location
DualCharacterSums.leanPaperXI/
55 lines · 6 declaration locations
DualityLinear.leanPaperXI/
94 lines · 7 declaration locations
DyadicAbstract.leanPaperXI/
159 lines · 16 declaration locations
DyadicAbstractOrthogonal.leanPaperXI/
141 lines · 9 declaration locations
DyadicAffine.leanPaperXI/
81 lines · 12 declaration locations
DyadicBasis.leanPaperXI/
83 lines · 9 declaration locations
DyadicBasisConsequences.leanPaperXI/
68 lines · 5 declaration locations
DyadicBasisCounts.leanPaperXI/
35 lines · 3 declaration locations
DyadicCoordinates.leanPaperXI/
162 lines · 19 declaration locations
DyadicCounts.leanPaperXI/
135 lines · 15 declaration locations
DyadicDimension.leanPaperXI/
49 lines · 5 declaration locations
DyadicExtensionClass.leanPaperXI/
93 lines · 7 declaration locations
DyadicGauss.leanPaperXI/
60 lines · 12 declaration locations
DyadicHeisenbergLift.leanPaperXI/
155 lines · 13 declaration locations
DyadicIsometry.leanPaperXI/
52 lines · 5 declaration locations
DyadicOrthogonal.leanPaperXI/
76 lines · 8 declaration locations
DyadicRefinement.leanPaperXI/
48 lines · 6 declaration locations
DyadicRefinementCounts.leanPaperXI/
55 lines · 8 declaration locations
DyadicTorsor.leanPaperXI/
70 lines · 11 declaration locations
DyadicTranslation.leanPaperXI/
89 lines · 13 declaration locations
ElementaryEnvelope.leanPaperXI/
139 lines · 20 declaration locations
ElementaryEnvelopeForm.leanPaperXI/
137 lines · 17 declaration locations
ElementaryEnvelopeTransport.leanPaperXI/
148 lines · 14 declaration locations
EquivariantRepresentation113.leanPaperXI/
117 lines · 2 declaration locations
EquivariantSplitting68.leanPaperXI/
35 lines · 1 declaration location
FiniteAverage.leanPaperXI/
69 lines · 9 declaration locations
FiniteBreakAssembly.leanPaperXI/
175 lines · 15 declaration locations
FiniteFieldAverage.leanPaperXI/
186 lines · 24 declaration locations
FiniteFieldOrbitCount.leanPaperXI/
93 lines · 12 declaration locations
FiniteFreeCompletion.leanPaperXI/
75 lines · 5 declaration locations
FiniteFunctionAverage.leanPaperXI/
54 lines · 4 declaration locations
FiniteIntersectionCriterion108.leanPaperXI/
30 lines · 1 declaration location
FiniteJointQuotient108.leanPaperXI/
47 lines · 8 declaration locations
FiniteOrbitAverage68.leanPaperXI/
101 lines · 7 declaration locations
FiniteProductDeterminant.leanPaperXI/
64 lines · 3 declaration locations
FiniteProfileBridge109.leanPaperXI/
195 lines · 15 declaration locations
FiniteRepresentation.leanPaperXI/
43 lines · 3 declaration locations
FiniteResidueBaseChange.leanPaperXI/
91 lines · 12 declaration locations
FiniteResidueSubgroup.leanPaperXI/
128 lines · 11 declaration locations
FiniteTameComparison.leanPaperXI/
113 lines · 6 declaration locations
FiniteTensor.leanPaperXI/
69 lines · 7 declaration locations
FiniteUnramifiedWeil.leanPaperXI/
198 lines · 19 declaration locations
FixedMoving.leanPaperXI/
198 lines · 27 declaration locations
FixedMovingSource.leanPaperXI/
111 lines · 16 declaration locations
FourierCovariance.leanPaperXI/
40 lines · 3 declaration locations
FourierPackets.leanPaperXI/
50 lines · 5 declaration locations
FourierProjectors.leanPaperXI/
79 lines · 8 declaration locations
FractionMatrix106.leanPaperXI/
57 lines · 2 declaration locations
FreeLatticeCard110.leanPaperXI/
55 lines · 4 declaration locations
FrobeniusOrbit.leanPaperXI/
42 lines · 9 declaration locations
FrobeniusPeriod.leanPaperXI/
97 lines · 12 declaration locations
FrobeniusPeriodCount.leanPaperXI/
125 lines · 11 declaration locations
FullBridgeTransport.leanPaperXI/
50 lines · 2 declaration locations
FullIntertwiningLocus69.leanPaperXI/
95 lines · 8 declaration locations
FullTypeIntertwining105.leanPaperXI/
151 lines · 7 declaration locations
GallagherTensorIrreducibility58.leanPaperXI/
165 lines · 7 declaration locations
GaussCharacters.leanPaperXI/
67 lines · 9 declaration locations
GaussSums.leanPaperXI/
90 lines · 11 declaration locations
GeneralChain.leanPaperXI/
89 lines · 8 declaration locations
GeneratedIrreducibility.leanPaperXI/
55 lines · 6 declaration locations
GlobalHeisenbergBridge112.leanPaperXI/
301 lines · 11 declaration locations
GluedPacketSections.leanPaperXI/
170 lines · 15 declaration locations
GraphChordCharacters.leanPaperXI/
144 lines · 16 declaration locations
GraphGauge.leanPaperXI/
190 lines · 19 declaration locations
GraphLoop.leanPaperXI/
106 lines · 19 declaration locations
GraphLoopRepresentation.leanPaperXI/
138 lines · 14 declaration locations
GraphResidual.leanPaperXI/
274 lines · 24 declaration locations
GraphTransport.leanPaperXI/
150 lines · 20 declaration locations
GraphTree.leanPaperXI/
245 lines · 32 declaration locations
GraphTreePaths.leanPaperXI/
87 lines · 5 declaration locations
GroupFixed.leanPaperXI/
85 lines · 4 declaration locations
HeisenbergCardinality.leanPaperXI/
65 lines · 8 declaration locations
HeisenbergCenter.leanPaperXI/
64 lines · 3 declaration locations
HeisenbergCharacterProfile111.leanPaperXI/
317 lines · 18 declaration locations
HeisenbergCochain.leanPaperXI/
69 lines · 6 declaration locations
HeisenbergComparison.leanPaperXI/
92 lines · 4 declaration locations
HeisenbergDimension.leanPaperXI/
41 lines · 6 declaration locations
HeisenbergFinite.leanPaperXI/
32 lines · 3 declaration locations
HeisenbergForm.leanPaperXI/
50 lines · 4 declaration locations
HeisenbergFrequency.leanPaperXI/
197 lines · 9 declaration locations
HeisenbergGeometry.leanPaperXI/
82 lines · 7 declaration locations
HeisenbergGroup.leanPaperXI/
109 lines · 33 declaration locations
HeisenbergNormalForm.leanPaperXI/
33 lines · 3 declaration locations
HeisenbergPrime.leanPaperXI/
29 lines · 3 declaration locations
HeisenbergProjector.leanPaperXI/
230 lines · 29 declaration locations
HeisenbergReduction107.leanPaperXI/
61 lines · 3 declaration locations
HeisenbergRepresentation.leanPaperXI/
72 lines · 9 declaration locations
HeisenbergSelector.leanPaperXI/
109 lines · 9 declaration locations
HeisenbergSource.leanPaperXI/
63 lines · 8 declaration locations
HeisenbergSourceProjector.leanPaperXI/
118 lines · 10 declaration locations
HeisenbergTensor.leanPaperXI/
99 lines · 9 declaration locations
HeisenbergTensorComparison.leanPaperXI/
70 lines · 5 declaration locations
HeisenbergTensorFactorization.leanPaperXI/
87 lines · 8 declaration locations
HeisenbergTrace108.leanPaperXI/
47 lines · 3 declaration locations
HeisenbergTransport.leanPaperXI/
180 lines · 23 declaration locations
HenselianConductorTransport.leanPaperXI/
120 lines · 9 declaration locations
HenselianFieldLift.leanPaperXI/
95 lines · 11 declaration locations
HenselianGaloisResidue.leanPaperXI/
75 lines · 6 declaration locations
HenselianLiftTower.leanPaperXI/
71 lines · 5 declaration locations
HenselianResidueLift.leanPaperXI/
115 lines · 18 declaration locations
HenselianWeilAttachment.leanPaperXI/
140 lines · 13 declaration locations
HolonomyResidual.leanPaperXI/
57 lines · 6 declaration locations
HyperbolicDeterminant.leanPaperXI/
66 lines · 6 declaration locations
HyperbolicPhase.leanPaperXI/
56 lines · 3 declaration locations
HyperbolicSpace.leanPaperXI/
120 lines · 11 declaration locations
InducedClassification.leanPaperXI/
136 lines · 9 declaration locations
InducedCycleInvariants.leanPaperXI/
107 lines · 13 declaration locations
InducedDual.leanPaperXI/
42 lines · 3 declaration locations
InducedTameProfile.leanPaperXI/
187 lines · 10 declaration locations
InducedTwist.leanPaperXI/
103 lines · 11 declaration locations
InducedTypeSpace68.leanPaperXI/
142 lines · 13 declaration locations
InductionIrreducibility.leanPaperXI/
237 lines · 16 declaration locations
InertiaFixed.leanPaperXI/
90 lines · 7 declaration locations
InertiaQuotient.leanPaperXI/
98 lines · 9 declaration locations
IntegerRingComparison.leanPaperXI/
230 lines · 20 declaration locations
InteractionPolynomial.leanPaperXI/
77 lines · 4 declaration locations
IntersectionModel108.leanPaperXI/
62 lines · 6 declaration locations
IntertwiningAlong105.leanPaperXI/
78 lines · 10 declaration locations
IntertwiningSpace107.leanPaperXI/
81 lines · 5 declaration locations
InvariantAssembly.leanPaperXI/
48 lines · 4 declaration locations
InvariantPolynomial.leanPaperXI/
90 lines · 11 declaration locations
IsotypicEvaluation.leanPaperXI/
97 lines · 6 declaration locations
LatticeCongruenceTopology60.leanPaperXI/
144 lines · 11 declaration locations
LatticeMatrixTopology60.leanPaperXI/
152 lines · 12 declaration locations
LiftedEtale.leanPaperXI/
95 lines · 8 declaration locations
LiftedFullResidue.leanPaperXI/
115 lines · 14 declaration locations
LiftedResidueDegree.leanPaperXI/
82 lines · 9 declaration locations
LiftedResidueFrobenius.leanPaperXI/
67 lines · 8 declaration locations
LiftedValuationFinite.leanPaperXI/
78 lines · 8 declaration locations
LiftedValuationInertia.leanPaperXI/
51 lines · 1 declaration location
LineCharacter.leanPaperXI/
172 lines · 15 declaration locations
LocalFactorIdentification.leanPaperXI/
150 lines · 16 declaration locations
LocalFieldResidueExtension.leanPaperXI/
63 lines · 9 declaration locations
LocalResidueRank.leanPaperXI/
83 lines · 5 declaration locations
LocallyFiniteSemisimple.leanPaperXI/
108 lines · 7 declaration locations
MonicResidueAlgebra.leanPaperXI/
87 lines · 14 declaration locations
MonodromyAtom.leanPaperXI/
117 lines · 12 declaration locations
MonodromyChain.leanPaperXI/
122 lines · 14 declaration locations
MonomialAction.leanPaperXI/
92 lines · 10 declaration locations
MonomialDual.leanPaperXI/
46 lines · 2 declaration locations
MonomialInduction.leanPaperXI/
152 lines · 19 declaration locations
MonomialInductionSubgroup.leanPaperXI/
69 lines · 3 declaration locations
MonomialInductionTransitive.leanPaperXI/
69 lines · 8 declaration locations
MonomialOrbit.leanPaperXI/
82 lines · 10 declaration locations
MoritaActualCartan110.leanPaperXI/
266 lines · 14 declaration locations
MoritaCartanTransport110.leanPaperXI/
121 lines · 14 declaration locations
MoritaCornerRank110.leanPaperXI/
132 lines · 7 declaration locations
MoritaEndomorphismCoordinates111.leanPaperXI/
176 lines · 14 declaration locations
MoritaIndex110.leanPaperXI/
144 lines · 6 declaration locations
MoritaLattice110.leanPaperXI/
354 lines · 31 declaration locations
MoritaPairIndex110.leanPaperXI/
39 lines · 1 declaration location
MoritaQuotient110.leanPaperXI/
170 lines · 21 declaration locations
MoritaRadicalDictionary110.leanPaperXI/
132 lines · 10 declaration locations
MoritaScalarUpgrade110.leanPaperXI/
55 lines · 4 declaration locations
MoritaUniformizer110.leanPaperXI/
62 lines · 10 declaration locations
MovingPhase.leanPaperXI/
87 lines · 10 declaration locations
NormalInertia.leanPaperXI/
85 lines · 7 declaration locations
NormalizedFrobeniusQuotient.leanPaperXI/
120 lines · 19 declaration locations
NormalizerDictionary110.leanPaperXI/
432 lines · 24 declaration locations
NormalizerExtensionInducing58.leanPaperXI/
272 lines · 31 declaration locations
NormalizerIntertwining60.leanPaperXI/
111 lines · 9 declaration locations
OddEnvelopeHeisenberg.leanPaperXI/
52 lines · 5 declaration locations
OddPhase.leanPaperXI/
89 lines · 16 declaration locations
OddPhaseCertificate.leanPaperXI/
61 lines · 6 declaration locations
OddPhaseSum.leanPaperXI/
92 lines · 10 declaration locations
OddPhaseTransport.leanPaperXI/
72 lines · 7 declaration locations
OddSymplectic.leanPaperXI/
70 lines · 6 declaration locations
OnePlusIndex110.leanPaperXI/
87 lines · 5 declaration locations
OnePlusIntersection110.leanPaperXI/
197 lines · 16 declaration locations
OpenSubgroupSmoothInduction.leanPaperXI/
409 lines · 33 declaration locations
OrbitSpan.leanPaperXI/
86 lines · 11 declaration locations
OrthogonalPhase.leanPaperXI/
111 lines · 8 declaration locations
OrthogonalSummands.leanPaperXI/
120 lines · 10 declaration locations
PacketBasis.leanPaperXI/
97 lines · 7 declaration locations
PacketCycle.leanPaperXI/
76 lines · 5 declaration locations
PacketLines.leanPaperXI/
147 lines · 11 declaration locations
PacketReturn.leanPaperXI/
61 lines · 4 declaration locations
PacketSupport.leanPaperXI/
105 lines · 7 declaration locations
PacketTransport.leanPaperXI/
81 lines · 10 declaration locations
PacketTypeAttachment70.leanPaperXI/
85 lines · 7 declaration locations
PairIndex110.leanPaperXI/
122 lines · 13 declaration locations
PeriodicLatticeReduction60.leanPaperXI/
86 lines · 4 declaration locations
PiPolynomial.leanPaperXI/
58 lines · 2 declaration locations
PolynomialAssembly.leanPaperXI/
83 lines · 7 declaration locations
PrescribedFieldType70.leanPaperXI/
87 lines · 4 declaration locations
PrimitiveCharacterBlock.leanPaperXI/
128 lines · 10 declaration locations
ProductNormalizerQuotient59.leanPaperXI/
95 lines · 7 declaration locations
ProjectiveCocycle.leanPaperXI/
171 lines · 12 declaration locations
ProjectiveHolonomy.leanPaperXI/
173 lines · 19 declaration locations
ProjectorTransport.leanPaperXI/
27 lines · 2 declaration locations
QuotientRepresentation.leanPaperXI/
72 lines · 9 declaration locations
RadicalOnePlus111.leanPaperXI/
58 lines · 5 declaration locations
RamificationPolyphase.leanPaperXI/
326 lines · 22 declaration locations
RamificationPolyphaseBaseChange.leanPaperXI/
115 lines · 7 declaration locations
RamificationPolyphaseDimensions.leanPaperXI/
180 lines · 11 declaration locations
RamificationSeparation.leanPaperXI/
78 lines · 4 declaration locations
RamifiedUnramifiedQuotient.leanPaperXI/
322 lines · 28 declaration locations
RankOneEulerFactor.leanPaperXI/
113 lines · 8 declaration locations
RankOneSourceCandidate110.leanPaperXI/
77 lines · 1 declaration location
RegularCyclic.leanPaperXI/
90 lines · 10 declaration locations
RepresentationGraph.leanPaperXI/
106 lines · 8 declaration locations
RepresentationStability.leanPaperXI/
47 lines · 4 declaration locations
ResidueDegreeBaseChange.leanPaperXI/
148 lines · 16 declaration locations
ResidueExtensionRealization.leanPaperXI/
97 lines · 19 declaration locations
ResidueFrobeniusAttachment.leanPaperXI/
144 lines · 22 declaration locations
ResidueRestriction107.leanPaperXI/
75 lines · 4 declaration locations
ResidueWeil.leanPaperXI/
114 lines · 13 declaration locations
RestrictedHeisenbergBridge.leanPaperXI/
84 lines · 2 declaration locations
ScalarCocycle112.leanPaperXI/
195 lines · 24 declaration locations
ScalarCovariance.leanPaperXI/
52 lines · 5 declaration locations
ScalarGluing.leanPaperXI/
167 lines · 13 declaration locations
ScalarHolonomy.leanPaperXI/
152 lines · 20 declaration locations
ScalarRepresentation112.leanPaperXI/
373 lines · 25 declaration locations
SchrodingerConsequences.leanPaperXI/
151 lines · 15 declaration locations
SchrodingerFourier.leanPaperXI/
77 lines · 3 declaration locations
SchrodingerIrreducible.leanPaperXI/
88 lines · 2 declaration locations
SchrodingerOperator.leanPaperXI/
93 lines · 12 declaration locations
SchrodingerSeparation.leanPaperXI/
32 lines · 1 declaration location
SchrodingerTrace.leanPaperXI/
88 lines · 7 declaration locations
SchrodingerUnitary.leanPaperXI/
45 lines · 3 declaration locations
SchrodingerUniversal.leanPaperXI/
217 lines · 19 declaration locations
SchurHom.leanPaperXI/
68 lines · 5 declaration locations
SchurScalar.leanPaperXI/
66 lines · 4 declaration locations
SemisimpleDetection.leanPaperXI/
71 lines · 3 declaration locations
SemisimpleProjection.leanPaperXI/
99 lines · 4 declaration locations
SimpleModuleClassification.leanPaperXI/
106 lines · 10 declaration locations
SingleCandidateComparison.leanPaperXI/
27 lines · 1 declaration location
SmithMatrix106.leanPaperXI/
57 lines · 3 declaration locations
SmoothDegreeQuotient.leanPaperXI/
192 lines · 24 declaration locations
SmoothHomOrbit68.leanPaperXI/
95 lines · 5 declaration locations
SpectralGeometricFrobenius.leanPaperXI/
184 lines · 25 declaration locations
SpectralLocalField.leanPaperXI/
175 lines · 24 declaration locations
SplitRadical105.leanPaperXI/
152 lines · 16 declaration locations
SymplecticAssembly.leanPaperXI/
51 lines · 4 declaration locations
SymplecticCentralExtension.leanPaperXI/
75 lines · 6 declaration locations
SymplecticCoordinates.leanPaperXI/
70 lines · 4 declaration locations
SymplecticHeisenbergUniqueness.leanPaperXI/
85 lines · 6 declaration locations
SymplecticSplit.leanPaperXI/
126 lines · 4 declaration locations
TameConductor.leanPaperXI/
113 lines · 10 declaration locations
TameDegree.leanPaperXI/
170 lines · 31 declaration locations
TameExponent.leanPaperXI/
117 lines · 11 declaration locations
TameGaussNaturality.leanPaperXI/
79 lines · 9 declaration locations
TameHomCriterion.leanPaperXI/
66 lines · 2 declaration locations
TameNorm.leanPaperXI/
102 lines · 13 declaration locations
TameNormPacket.leanPaperXI/
118 lines · 8 declaration locations
TameOrbitTransitivity.leanPaperXI/
110 lines · 8 declaration locations
TameProjectors.leanPaperXI/
86 lines · 11 declaration locations
TameTensorInduction.leanPaperXI/
111 lines · 7 declaration locations
TameTensorOrbits.leanPaperXI/
210 lines · 31 declaration locations
TameTensorPackets.leanPaperXI/
81 lines · 10 declaration locations
TameTensorSource.leanPaperXI/
122 lines · 11 declaration locations
TensorFixed.leanPaperXI/
34 lines · 1 declaration location
TensorIntertwining107.leanPaperXI/
106 lines · 6 declaration locations
TensorIrreducible.leanPaperXI/
78 lines · 4 declaration locations
TensorPolynomial.leanPaperXI/
89 lines · 7 declaration locations
TensorSlices107.leanPaperXI/
115 lines · 13 declaration locations
TensorSubspace.leanPaperXI/
76 lines · 8 declaration locations
TensorTypeOperators70.leanPaperXI/
94 lines · 14 declaration locations
TraceDiscrepancy.leanPaperXI/
84 lines · 8 declaration locations
TranslationAverage.leanPaperXI/
102 lines · 12 declaration locations
TwistedAction.leanPaperXI/
79 lines · 8 declaration locations
TwistedActionEquivalence.leanPaperXI/
107 lines · 11 declaration locations
TwistedAlgebra.leanPaperXI/
109 lines · 15 declaration locations
TwistedMatrix.leanPaperXI/
54 lines · 4 declaration locations
TwistedModules.leanPaperXI/
54 lines · 5 declaration locations
TwistedRegular.leanPaperXI/
81 lines · 8 declaration locations
TwistedRescaling.leanPaperXI/
158 lines · 14 declaration locations
TwistedSimple.leanPaperXI/
205 lines · 10 declaration locations
TypeNormalizerAction.leanPaperXI/
108 lines · 11 declaration locations
TypeNormalizerForm.leanPaperXI/
85 lines · 5 declaration locations
TypeNormalizerPairing.leanPaperXI/
154 lines · 12 declaration locations
TypeProjectiveImplementation.leanPaperXI/
157 lines · 12 declaration locations
TypeSideDescent.leanPaperXI/
293 lines · 33 declaration locations
TypeSideExtension.leanPaperXI/
170 lines · 12 declaration locations
TypeSideUniqueness.leanPaperXI/
96 lines · 4 declaration locations
UnramifiedBaseChangeFactor.leanPaperXI/
159 lines · 13 declaration locations
UnramifiedConductor.leanPaperXI/
131 lines · 12 declaration locations
UnramifiedConductorZero.leanPaperXI/
109 lines · 7 declaration locations
UnramifiedFieldTower.leanPaperXI/
270 lines · 20 declaration locations
UnramifiedLocalFactor.leanPaperXI/
168 lines · 20 declaration locations
UnramifiedPolynomial.leanPaperXI/
90 lines · 15 declaration locations
UnramifiedValuation.leanPaperXI/
145 lines · 11 declaration locations
ValuationConductor.leanPaperXI/
167 lines · 18 declaration locations
ValuationFixingField.leanPaperXI/
41 lines · 4 declaration locations
ValuationIntegralModel.leanPaperXI/
72 lines · 11 declaration locations
ValuationRamification.leanPaperXI/
96 lines · 9 declaration locations
ValuationResidueEmbedding.leanPaperXI/
48 lines · 7 declaration locations
ValuationTameEndpoint.leanPaperXI/
52 lines · 5 declaration locations
PaperXIAdditions.lean
1 line · 0 declaration locations
PaperXITerminal.lean
1 line · 0 declaration locations
ActualMonomialLocalGlobal.import_only.leanterminal_original/
470 lines · 30 declaration locations
ActualMonomialLocalGlobal.leanterminal_original/
469 lines · 30 declaration locations