Map

How this project builds on itself. An arrow goes from a file to a file that uses something in it, so the foundations are on the left. These links come from names in the source code, not from kernel dependency facts; the separate Trust page says exactly what Lean checked. every declaration's own map, on its file page, shows the same thing one result at a time.

Files as a table

The same map data in a searchable keyboard- and screen-reader-friendly form.

Files and cross-file dependency counts
FileDeclarationsBuilds onUsed by
FLT/Assumptions/KnownIn1980s.lean102
FLT/Assumptions/Mazur.lean100
FLT/Assumptions/Odlyzko.lean100
FLT/AutomorphicForm/GroupTheoryStuff.lean4504
FLT/AutomorphicForm/QuaternionAlgebra/Basic.lean10092
FLT/AutomorphicForm/QuaternionAlgebra/FiniteDimensional.lean120
FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Abstract.lean1501
FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean4892
FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Local.lean1221
FLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean6350
FLT/AutomorphicForm/Stuff.lean2606
FLT/Basic/Lemmas.lean302
FLT/Data/Hurwitz.lean8300
FLT/Data/HurwitzRatHat.lean910
FLT/Data/QHat.lean5502
FLT/DedekindDomain/AdicValuation.lean2822
FLT/DedekindDomain/Completion/BaseChange.lean43110
FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean27111
FLT/DedekindDomain/FiniteAdeleRing/IsDirectLimitRestricted.lean420
FLT/DedekindDomain/FiniteAdeleRing/LocalUnits.lean1100
FLT/DedekindDomain/FiniteAdeleRing/TensorPi.lean902
FLT/DedekindDomain/FiniteAdeleRing/TensorProduct.lean531
FLT/DedekindDomain/FiniteAdeleRing/TensorRestrictedProduct.lean1631
FLT/DedekindDomain/IntegralClosure.lean2413
FLT/Deformations/Algebra/InverseLimit/Basic.lean2801
FLT/Deformations/Algebra/InverseLimit/Topology.lean310
FLT/Deformations/Categories.lean2642
FLT/Deformations/ContinuousRepresentation/IsTopologicalModule.lean401
FLT/Deformations/IsProartinian.lean621
FLT/Deformations/IsResidueAlgebra.lean1001
FLT/Deformations/Lemmas.lean2705
FLT/Deformations/LiftFunctor.lean1441
FLT/Deformations/Representable.lean620
FLT/Deformations/RepresentationTheory/AbsoluteGaloisGroup.lean1023
FLT/Deformations/RepresentationTheory/Frobenius.lean500
FLT/Deformations/RepresentationTheory/GaloisRep.lean45312
FLT/Deformations/RepresentationTheory/GaloisRepFamily.lean211
FLT/Deformations/RepresentationTheory/IntegralClosure.lean612
FLT/Deformations/RepresentationTheory/Irreducible.lean100
FLT/Deformations/Subfunctor.lean100
FLT/DivisionAlgebra/Finiteness.lean80120
FLT/EllipticCurve/Torsion.lean1110
FLT/FreyCurve/Basic.lean1211
FLT/FreyCurve/FreyPackage.lean903
FLT/FreyCurve/Mazur.lean141
FLT/GaloisRepresentation/Automorphic.lean260
FLT/GaloisRepresentation/Cyclotomic.lean610
FLT/GaloisRepresentation/HardlyRamified/Defs.lean225
FLT/GaloisRepresentation/HardlyRamified/Family.lean130
FLT/GaloisRepresentation/HardlyRamified/Frey.lean220
FLT/GaloisRepresentation/HardlyRamified/Lift.lean120
FLT/GaloisRepresentation/HardlyRamified/ModThree.lean120
FLT/GaloisRepresentation/HardlyRamified/Threeadic.lean120
FLT/GlobalLanglandsConjectures/GLnDefs.lean2301
FLT/GlobalLanglandsConjectures/GLzero.lean510
FLT/HaarMeasure/FiniteAdeleRing.lean1130
FLT/HaarMeasure/HaarChar/AddEquiv.lean1111
FLT/HaarMeasure/HaarChar/AdeleRing.lean9111
FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean2671
FLT/HaarMeasure/HaarChar/FiniteDimensional.lean1042
FLT/HaarMeasure/HaarChar/Padic.lean631
FLT/HaarMeasure/HaarChar/RealComplex.lean412
FLT/HaarMeasure/HaarChar/Ring.lean1726
FLT/HaarMeasure/MeasurableSpacePadics.lean1611
FLT/HaarMeasure/Quotient.lean1930
FLT/Hacks/RightActionInstances.lean1409
FLT/HenselianLocalRing/EtaleDecomposition.lean300
FLT/HenselianLocalRing/Finite.lean1400
FLT/HenselianLocalRing/Stuff.lean600
FLT/KnownIn1980s/EllipticCurves/Flat.lean300
FLT/KnownIn1980s/EllipticCurves/GoodReduction.lean100
FLT/KnownIn1980s/EllipticCurves/QuadraticTwists/QuadraticTwists.lean3871
FLT/KnownIn1980s/EllipticCurves/QuadraticTwists/SplitMultiplicativeReduction.lean1170
FLT/KnownIn1980s/EllipticCurves/ReductionBaseChange.lean1020
FLT/KnownIn1980s/EllipticCurves/TateCurve.lean3420
FLT/KnownIn1980s/EllipticCurves/TateCurveBaseChange.lean1131
FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean12800
FLT/KnownIn1980s/EllipticCurves/TateParameter.lean2212
FLT/KnownIn1980s/EllipticCurves/Torsion.lean100
FLT/KnownIn1980s/EllipticCurves/WeilPairing.lean100
FLT/KnownIn1980s/PGL2/Defs.lean503
FLT/KnownIn1980s/PGL2/Proofs.lean230
FLT/KnownIn1980s/RepresentationTheory/OddAbsIrred.lean110
FLT/Mathlib/Algebra/Algebra/Bilinear.lean1122
FLT/Mathlib/Algebra/Algebra/Equiv.lean100
FLT/Mathlib/Algebra/Algebra/Hom.lean2005
FLT/Mathlib/Algebra/Algebra/Pi.lean1604
FLT/Mathlib/Algebra/Algebra/Tower.lean905
FLT/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean502
FLT/Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean1712
FLT/Mathlib/Algebra/Central/TensorProduct.lean500
FLT/Mathlib/Algebra/FixedPoints/Basic.lean1200
FLT/Mathlib/Algebra/Group/Action/Hom.lean501
FLT/Mathlib/Algebra/Homology/HomologicalComplex.lean101
FLT/Mathlib/Algebra/IsDirectLimit.lean1902
FLT/Mathlib/Algebra/IsQuaternionAlgebra.lean1003
FLT/Mathlib/Algebra/Module/Submodule/Basic.lean101
FLT/Mathlib/Algebra/Module/TransferInstance.lean200
FLT/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean1301
FLT/Mathlib/Algebra/Polynomial/QuadraticDiscriminant.lean611
FLT/Mathlib/Algebra/Polynomial/Splits.lean101
FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean1701
FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Aut.lean820
FLT/Mathlib/AlgebraicGeometry/EllipticCurve/GaloisDescent.lean211
FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Reduction.lean2522
FLT/Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean1212
FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean403
FLT/Mathlib/Data/Fin/Basic.lean100
FLT/Mathlib/Data/Real/Archimedean.lean101
FLT/Mathlib/Data/Set/Prod.lean100
FLT/Mathlib/FieldTheory/Galois/Basic.lean1203
FLT/Mathlib/FieldTheory/Galois/Infinite.lean630
FLT/Mathlib/FieldTheory/Separable.lean101
FLT/Mathlib/FieldTheory/SeparableDegree.lean100
FLT/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean201
FLT/Mathlib/GroupTheory/DoubleCoset.lean4024
FLT/Mathlib/GroupTheory/GroupAction/Quotient.lean201
FLT/Mathlib/GroupTheory/Index.lean100
FLT/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean101
FLT/Mathlib/LinearAlgebra/Countable.lean100
FLT/Mathlib/LinearAlgebra/Determinant.lean901
FLT/Mathlib/LinearAlgebra/Dimension/Constructions.lean313
FLT/Mathlib/LinearAlgebra/Dimension/IsQuadraticExtension.lean401
FLT/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean1103
FLT/Mathlib/LinearAlgebra/Matrix/Transvection.lean1002
FLT/Mathlib/LinearAlgebra/Pi.lean704
FLT/Mathlib/LinearAlgebra/TensorProduct/Algebra.lean202
FLT/Mathlib/LinearAlgebra/TensorProduct/FiniteFree.lean101
FLT/Mathlib/MeasureTheory/Group/Action.lean500
FLT/Mathlib/MeasureTheory/Group/Measure.lean100
FLT/Mathlib/MeasureTheory/Group/ModularCharacter.lean3033
FLT/Mathlib/MeasureTheory/Haar/Extension.lean200
FLT/Mathlib/MeasureTheory/Measure/Regular.lean300
FLT/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean100
FLT/Mathlib/NumberTheory/NumberField/AdeleRing.lean900
FLT/Mathlib/NumberTheory/NumberField/FiniteAdeleRing.lean211
FLT/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean501
FLT/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean101
FLT/Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean100
FLT/Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean901
FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean1302
FLT/Mathlib/Order/Filter/Cofinite.lean100
FLT/Mathlib/RepresentationTheory/Basic.lean300
FLT/Mathlib/RepresentationTheory/Continuous/Basic.lean312
FLT/Mathlib/RepresentationTheory/Continuous/TopRep.lean111
FLT/Mathlib/RepresentationTheory/Homological/ContCohomology/Basic.lean2021
FLT/Mathlib/RepresentationTheory/Homological/ContCohomology/CupProduct.lean3350
FLT/Mathlib/RingTheory/AdjoinRoot.lean502
FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean302
FLT/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean2225
FLT/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean401
FLT/Mathlib/RingTheory/DiscreteValuationRing/AdjoinRoot.lean1102
FLT/Mathlib/RingTheory/DiscreteValuationRing/Separable.lean110
FLT/Mathlib/RingTheory/Ideal/Quotient/Basic.lean101
FLT/Mathlib/RingTheory/LocalRing/Defs.lean200
FLT/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean100
FLT/Mathlib/RingTheory/Localization/BaseChange.lean601
FLT/Mathlib/RingTheory/Norm/Quadratic.lean711
FLT/Mathlib/RingTheory/Norm/Quotient.lean301
FLT/Mathlib/RingTheory/Polynomial/GaussLemma.lean100
FLT/Mathlib/RingTheory/RamificationInertia/Basic.lean101
FLT/Mathlib/RingTheory/SimpleRing/TensorProduct.lean800
FLT/Mathlib/RingTheory/TensorProduct/Basis.lean411
FLT/Mathlib/RingTheory/TensorProduct/Pi.lean101
FLT/Mathlib/RingTheory/Unramified/LocalRing.lean121
FLT/Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean101
FLT/Mathlib/RingTheory/Valuation/ValuationSubring.lean401
FLT/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean803
FLT/Mathlib/Topology/Algebra/Algebra/Hom.lean1111
FLT/Mathlib/Topology/Algebra/ContinuousAlgEquiv.lean110
FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean612
FLT/Mathlib/Topology/Algebra/ContinuousSMulDiscrete.lean502
FLT/Mathlib/Topology/Algebra/Group/Basic.lean301
FLT/Mathlib/Topology/Algebra/Group/Quotient.lean201
FLT/Mathlib/Topology/Algebra/Group/Units.lean101
FLT/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean100
FLT/Mathlib/Topology/Algebra/Module/Equiv.lean1413
FLT/Mathlib/Topology/Algebra/Module/FiniteDimension.lean101
FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean3329
FLT/Mathlib/Topology/Algebra/Module/Quotient.lean201
FLT/Mathlib/Topology/Algebra/Module/TensorProduct.lean712
FLT/Mathlib/Topology/Algebra/Monoid.lean200
FLT/Mathlib/Topology/Algebra/Order/Field.lean710
FLT/Mathlib/Topology/Algebra/RestrictedProduct/Algebra.lean310
FLT/Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean2309
FLT/Mathlib/Topology/Algebra/RestrictedProduct/Equiv.lean4315
FLT/Mathlib/Topology/Algebra/RestrictedProduct/Module.lean1441
FLT/Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean4845
FLT/Mathlib/Topology/Algebra/UniformRing.lean301
FLT/Mathlib/Topology/Algebra/ValuativeRel/ValuativeTopology.lean100
FLT/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean101
FLT/Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean611
FLT/Mathlib/Topology/Bases.lean101
FLT/Mathlib/Topology/CompactOpen.lean100
FLT/Mathlib/Topology/Constructions.lean311
FLT/Mathlib/Topology/HomToDiscrete.lean901
FLT/Mathlib/Topology/MetricSpace/Pseudo/Matrix.lean100
FLT/Mathlib/Topology/Polish.lean202
FLT/NumberField/AdeleRing.lean43162
FLT/NumberField/Completion/Finite.lean524
FLT/NumberField/Completion/Infinite.lean1690
FLT/NumberField/DiscriminantBounds.lean1700
FLT/NumberField/InfiniteAdeleRing.lean741
FLT/NumberField/InfinitePlace/Extension.lean3501
FLT/NumberField/Padics/RestrictedProduct.lean1011
FLT/Patching/Algebra.lean2832
FLT/Patching/Module.lean4842
FLT/Patching/Over.lean1151
FLT/Patching/REqualsT.lean110
FLT/Patching/System.lean1161
FLT/Patching/Ultraproduct.lean3135
FLT/Patching/Utils/AdicTopology.lean1204
FLT/Patching/Utils/CompactHausdorffRings.lean400
FLT/Patching/Utils/Depth.lean1301
FLT/Patching/Utils/InverseLimit.lean303
FLT/Patching/Utils/Lemmas.lean2804
FLT/Patching/Utils/StructureFiniteness.lean1301
FLT/Patching/Utils/TopologicallyFG.lean201
FLT/Patching/VanishingFilter.lean1110
FLT/Proof.lean1241
FLT/QuaternionAlgebra/NumberField.lean6265
FLT/Slop/DimensionTheorem/Defs.lean1114
FLT/Slop/DimensionTheorem/DimEqDelta.lean411
FLT/Slop/DimensionTheorem/DimLeGrowth.lean1021
FLT/Slop/DimensionTheorem/GrowthLeDelta.lean1021
FLT/Slop/DimensionTheorem/Main.lean440
FLT/Slop/DimensionTheorem/Numeric.lean803
FLT/Slop/NumberTheory/TsumDivisorsAntidiagonal.lean501
FLT/Slop/PGL2/FiniteSubgroups/CyclicPartition.lean3811
FLT/Slop/PGL2/FiniteSubgroups/DicksonClassification.lean130
FLT/Slop/PGL2/FiniteSubgroups/FieldReconstruction.lean9622
FLT/Slop/PGL2/FiniteSubgroups/NatClassEquation.lean701
FLT/Slop/PGL2/FiniteSubgroups/PGLBasic.lean38110
FLT/Slop/PGL2/FiniteSubgroups/PSLBasic.lean3411
FLT/Slop/PGL2/FiniteSubgroups/PSLRecognition.lean1631
FLT/Slop/PGL2/FiniteSubgroups/PartitionHelpers.lean2814
FLT/Slop/PGL2/FiniteSubgroups/PartitionProof.lean3031
FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean4512
FLT/Slop/PGL2/FiniteSubgroups/TameClassification.lean3432
FLT/Slop/PGL2/FiniteSubgroups/WildClassification.lean2582
FLT/Slop/RepresentationTheory/OddAbsIrredOrig.lean1210
FLT/Slop/RepresentationTheory/OddAbsIrredSlop.lean1202
FermatsLastTheorem.lean120