| FLT/Assumptions/KnownIn1980s.lean | 1 | 0 | 2 |
| FLT/Assumptions/Mazur.lean | 1 | 0 | 0 |
| FLT/Assumptions/Odlyzko.lean | 1 | 0 | 0 |
| FLT/AutomorphicForm/GroupTheoryStuff.lean | 45 | 0 | 4 |
| FLT/AutomorphicForm/QuaternionAlgebra/Basic.lean | 100 | 9 | 2 |
| FLT/AutomorphicForm/QuaternionAlgebra/FiniteDimensional.lean | 1 | 2 | 0 |
| FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Abstract.lean | 15 | 0 | 1 |
| FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean | 48 | 9 | 2 |
| FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Local.lean | 12 | 2 | 1 |
| FLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean | 63 | 5 | 0 |
| FLT/AutomorphicForm/Stuff.lean | 26 | 0 | 6 |
| FLT/Basic/Lemmas.lean | 3 | 0 | 2 |
| FLT/Data/Hurwitz.lean | 83 | 0 | 0 |
| FLT/Data/HurwitzRatHat.lean | 9 | 1 | 0 |
| FLT/Data/QHat.lean | 55 | 0 | 2 |
| FLT/DedekindDomain/AdicValuation.lean | 28 | 2 | 2 |
| FLT/DedekindDomain/Completion/BaseChange.lean | 43 | 11 | 0 |
| FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean | 27 | 11 | 1 |
| FLT/DedekindDomain/FiniteAdeleRing/IsDirectLimitRestricted.lean | 4 | 2 | 0 |
| FLT/DedekindDomain/FiniteAdeleRing/LocalUnits.lean | 11 | 0 | 0 |
| FLT/DedekindDomain/FiniteAdeleRing/TensorPi.lean | 9 | 0 | 2 |
| FLT/DedekindDomain/FiniteAdeleRing/TensorProduct.lean | 5 | 3 | 1 |
| FLT/DedekindDomain/FiniteAdeleRing/TensorRestrictedProduct.lean | 16 | 3 | 1 |
| FLT/DedekindDomain/IntegralClosure.lean | 24 | 1 | 3 |
| FLT/Deformations/Algebra/InverseLimit/Basic.lean | 28 | 0 | 1 |
| FLT/Deformations/Algebra/InverseLimit/Topology.lean | 3 | 1 | 0 |
| FLT/Deformations/Categories.lean | 26 | 4 | 2 |
| FLT/Deformations/ContinuousRepresentation/IsTopologicalModule.lean | 4 | 0 | 1 |
| FLT/Deformations/IsProartinian.lean | 6 | 2 | 1 |
| FLT/Deformations/IsResidueAlgebra.lean | 10 | 0 | 1 |
| FLT/Deformations/Lemmas.lean | 27 | 0 | 5 |
| FLT/Deformations/LiftFunctor.lean | 14 | 4 | 1 |
| FLT/Deformations/Representable.lean | 6 | 2 | 0 |
| FLT/Deformations/RepresentationTheory/AbsoluteGaloisGroup.lean | 10 | 2 | 3 |
| FLT/Deformations/RepresentationTheory/Frobenius.lean | 5 | 0 | 0 |
| FLT/Deformations/RepresentationTheory/GaloisRep.lean | 45 | 3 | 12 |
| FLT/Deformations/RepresentationTheory/GaloisRepFamily.lean | 2 | 1 | 1 |
| FLT/Deformations/RepresentationTheory/IntegralClosure.lean | 6 | 1 | 2 |
| FLT/Deformations/RepresentationTheory/Irreducible.lean | 1 | 0 | 0 |
| FLT/Deformations/Subfunctor.lean | 1 | 0 | 0 |
| FLT/DivisionAlgebra/Finiteness.lean | 80 | 12 | 0 |
| FLT/EllipticCurve/Torsion.lean | 11 | 1 | 0 |
| FLT/FreyCurve/Basic.lean | 12 | 1 | 1 |
| FLT/FreyCurve/FreyPackage.lean | 9 | 0 | 3 |
| FLT/FreyCurve/Mazur.lean | 1 | 4 | 1 |
| FLT/GaloisRepresentation/Automorphic.lean | 2 | 6 | 0 |
| FLT/GaloisRepresentation/Cyclotomic.lean | 6 | 1 | 0 |
| FLT/GaloisRepresentation/HardlyRamified/Defs.lean | 2 | 2 | 5 |
| FLT/GaloisRepresentation/HardlyRamified/Family.lean | 1 | 3 | 0 |
| FLT/GaloisRepresentation/HardlyRamified/Frey.lean | 2 | 2 | 0 |
| FLT/GaloisRepresentation/HardlyRamified/Lift.lean | 1 | 2 | 0 |
| FLT/GaloisRepresentation/HardlyRamified/ModThree.lean | 1 | 2 | 0 |
| FLT/GaloisRepresentation/HardlyRamified/Threeadic.lean | 1 | 2 | 0 |
| FLT/GlobalLanglandsConjectures/GLnDefs.lean | 23 | 0 | 1 |
| FLT/GlobalLanglandsConjectures/GLzero.lean | 5 | 1 | 0 |
| FLT/HaarMeasure/FiniteAdeleRing.lean | 11 | 3 | 0 |
| FLT/HaarMeasure/HaarChar/AddEquiv.lean | 11 | 1 | 1 |
| FLT/HaarMeasure/HaarChar/AdeleRing.lean | 9 | 11 | 1 |
| FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean | 26 | 7 | 1 |
| FLT/HaarMeasure/HaarChar/FiniteDimensional.lean | 10 | 4 | 2 |
| FLT/HaarMeasure/HaarChar/Padic.lean | 6 | 3 | 1 |
| FLT/HaarMeasure/HaarChar/RealComplex.lean | 4 | 1 | 2 |
| FLT/HaarMeasure/HaarChar/Ring.lean | 17 | 2 | 6 |
| FLT/HaarMeasure/MeasurableSpacePadics.lean | 16 | 1 | 1 |
| FLT/HaarMeasure/Quotient.lean | 19 | 3 | 0 |
| FLT/Hacks/RightActionInstances.lean | 14 | 0 | 9 |
| FLT/HenselianLocalRing/EtaleDecomposition.lean | 3 | 0 | 0 |
| FLT/HenselianLocalRing/Finite.lean | 14 | 0 | 0 |
| FLT/HenselianLocalRing/Stuff.lean | 6 | 0 | 0 |
| FLT/KnownIn1980s/EllipticCurves/Flat.lean | 3 | 0 | 0 |
| FLT/KnownIn1980s/EllipticCurves/GoodReduction.lean | 1 | 0 | 0 |
| FLT/KnownIn1980s/EllipticCurves/QuadraticTwists/QuadraticTwists.lean | 38 | 7 | 1 |
| FLT/KnownIn1980s/EllipticCurves/QuadraticTwists/SplitMultiplicativeReduction.lean | 11 | 7 | 0 |
| FLT/KnownIn1980s/EllipticCurves/ReductionBaseChange.lean | 10 | 2 | 0 |
| FLT/KnownIn1980s/EllipticCurves/TateCurve.lean | 34 | 2 | 0 |
| FLT/KnownIn1980s/EllipticCurves/TateCurveBaseChange.lean | 11 | 3 | 1 |
| FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean | 128 | 0 | 0 |
| FLT/KnownIn1980s/EllipticCurves/TateParameter.lean | 22 | 1 | 2 |
| FLT/KnownIn1980s/EllipticCurves/Torsion.lean | 1 | 0 | 0 |
| FLT/KnownIn1980s/EllipticCurves/WeilPairing.lean | 1 | 0 | 0 |
| FLT/KnownIn1980s/PGL2/Defs.lean | 5 | 0 | 3 |
| FLT/KnownIn1980s/PGL2/Proofs.lean | 2 | 3 | 0 |
| FLT/KnownIn1980s/RepresentationTheory/OddAbsIrred.lean | 1 | 1 | 0 |
| FLT/Mathlib/Algebra/Algebra/Bilinear.lean | 11 | 2 | 2 |
| FLT/Mathlib/Algebra/Algebra/Equiv.lean | 1 | 0 | 0 |
| FLT/Mathlib/Algebra/Algebra/Hom.lean | 20 | 0 | 5 |
| FLT/Mathlib/Algebra/Algebra/Pi.lean | 16 | 0 | 4 |
| FLT/Mathlib/Algebra/Algebra/Tower.lean | 9 | 0 | 5 |
| FLT/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean | 5 | 0 | 2 |
| FLT/Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean | 17 | 1 | 2 |
| FLT/Mathlib/Algebra/Central/TensorProduct.lean | 5 | 0 | 0 |
| FLT/Mathlib/Algebra/FixedPoints/Basic.lean | 12 | 0 | 0 |
| FLT/Mathlib/Algebra/Group/Action/Hom.lean | 5 | 0 | 1 |
| FLT/Mathlib/Algebra/Homology/HomologicalComplex.lean | 1 | 0 | 1 |
| FLT/Mathlib/Algebra/IsDirectLimit.lean | 19 | 0 | 2 |
| FLT/Mathlib/Algebra/IsQuaternionAlgebra.lean | 10 | 0 | 3 |
| FLT/Mathlib/Algebra/Module/Submodule/Basic.lean | 1 | 0 | 1 |
| FLT/Mathlib/Algebra/Module/TransferInstance.lean | 2 | 0 | 0 |
| FLT/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean | 13 | 0 | 1 |
| FLT/Mathlib/Algebra/Polynomial/QuadraticDiscriminant.lean | 6 | 1 | 1 |
| FLT/Mathlib/Algebra/Polynomial/Splits.lean | 1 | 0 | 1 |
| FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean | 17 | 0 | 1 |
| FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Aut.lean | 8 | 2 | 0 |
| FLT/Mathlib/AlgebraicGeometry/EllipticCurve/GaloisDescent.lean | 2 | 1 | 1 |
| FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Reduction.lean | 25 | 2 | 2 |
| FLT/Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean | 12 | 1 | 2 |
| FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean | 4 | 0 | 3 |
| FLT/Mathlib/Data/Fin/Basic.lean | 1 | 0 | 0 |
| FLT/Mathlib/Data/Real/Archimedean.lean | 1 | 0 | 1 |
| FLT/Mathlib/Data/Set/Prod.lean | 1 | 0 | 0 |
| FLT/Mathlib/FieldTheory/Galois/Basic.lean | 12 | 0 | 3 |
| FLT/Mathlib/FieldTheory/Galois/Infinite.lean | 6 | 3 | 0 |
| FLT/Mathlib/FieldTheory/Separable.lean | 1 | 0 | 1 |
| FLT/Mathlib/FieldTheory/SeparableDegree.lean | 1 | 0 | 0 |
| FLT/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean | 2 | 0 | 1 |
| FLT/Mathlib/GroupTheory/DoubleCoset.lean | 40 | 2 | 4 |
| FLT/Mathlib/GroupTheory/GroupAction/Quotient.lean | 2 | 0 | 1 |
| FLT/Mathlib/GroupTheory/Index.lean | 1 | 0 | 0 |
| FLT/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean | 1 | 0 | 1 |
| FLT/Mathlib/LinearAlgebra/Countable.lean | 1 | 0 | 0 |
| FLT/Mathlib/LinearAlgebra/Determinant.lean | 9 | 0 | 1 |
| FLT/Mathlib/LinearAlgebra/Dimension/Constructions.lean | 3 | 1 | 3 |
| FLT/Mathlib/LinearAlgebra/Dimension/IsQuadraticExtension.lean | 4 | 0 | 1 |
| FLT/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean | 11 | 0 | 3 |
| FLT/Mathlib/LinearAlgebra/Matrix/Transvection.lean | 10 | 0 | 2 |
| FLT/Mathlib/LinearAlgebra/Pi.lean | 7 | 0 | 4 |
| FLT/Mathlib/LinearAlgebra/TensorProduct/Algebra.lean | 2 | 0 | 2 |
| FLT/Mathlib/LinearAlgebra/TensorProduct/FiniteFree.lean | 1 | 0 | 1 |
| FLT/Mathlib/MeasureTheory/Group/Action.lean | 5 | 0 | 0 |
| FLT/Mathlib/MeasureTheory/Group/Measure.lean | 1 | 0 | 0 |
| FLT/Mathlib/MeasureTheory/Group/ModularCharacter.lean | 30 | 3 | 3 |
| FLT/Mathlib/MeasureTheory/Haar/Extension.lean | 2 | 0 | 0 |
| FLT/Mathlib/MeasureTheory/Measure/Regular.lean | 3 | 0 | 0 |
| FLT/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean | 1 | 0 | 0 |
| FLT/Mathlib/NumberTheory/NumberField/AdeleRing.lean | 9 | 0 | 0 |
| FLT/Mathlib/NumberTheory/NumberField/FiniteAdeleRing.lean | 2 | 1 | 1 |
| FLT/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean | 5 | 0 | 1 |
| FLT/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean | 1 | 0 | 1 |
| FLT/Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean | 1 | 0 | 0 |
| FLT/Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean | 9 | 0 | 1 |
| FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean | 13 | 0 | 2 |
| FLT/Mathlib/Order/Filter/Cofinite.lean | 1 | 0 | 0 |
| FLT/Mathlib/RepresentationTheory/Basic.lean | 3 | 0 | 0 |
| FLT/Mathlib/RepresentationTheory/Continuous/Basic.lean | 3 | 1 | 2 |
| FLT/Mathlib/RepresentationTheory/Continuous/TopRep.lean | 1 | 1 | 1 |
| FLT/Mathlib/RepresentationTheory/Homological/ContCohomology/Basic.lean | 20 | 2 | 1 |
| FLT/Mathlib/RepresentationTheory/Homological/ContCohomology/CupProduct.lean | 33 | 5 | 0 |
| FLT/Mathlib/RingTheory/AdjoinRoot.lean | 5 | 0 | 2 |
| FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean | 3 | 0 | 2 |
| FLT/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean | 22 | 2 | 5 |
| FLT/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean | 4 | 0 | 1 |
| FLT/Mathlib/RingTheory/DiscreteValuationRing/AdjoinRoot.lean | 11 | 0 | 2 |
| FLT/Mathlib/RingTheory/DiscreteValuationRing/Separable.lean | 1 | 1 | 0 |
| FLT/Mathlib/RingTheory/Ideal/Quotient/Basic.lean | 1 | 0 | 1 |
| FLT/Mathlib/RingTheory/LocalRing/Defs.lean | 2 | 0 | 0 |
| FLT/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean | 1 | 0 | 0 |
| FLT/Mathlib/RingTheory/Localization/BaseChange.lean | 6 | 0 | 1 |
| FLT/Mathlib/RingTheory/Norm/Quadratic.lean | 7 | 1 | 1 |
| FLT/Mathlib/RingTheory/Norm/Quotient.lean | 3 | 0 | 1 |
| FLT/Mathlib/RingTheory/Polynomial/GaussLemma.lean | 1 | 0 | 0 |
| FLT/Mathlib/RingTheory/RamificationInertia/Basic.lean | 1 | 0 | 1 |
| FLT/Mathlib/RingTheory/SimpleRing/TensorProduct.lean | 8 | 0 | 0 |
| FLT/Mathlib/RingTheory/TensorProduct/Basis.lean | 4 | 1 | 1 |
| FLT/Mathlib/RingTheory/TensorProduct/Pi.lean | 1 | 0 | 1 |
| FLT/Mathlib/RingTheory/Unramified/LocalRing.lean | 1 | 2 | 1 |
| FLT/Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean | 1 | 0 | 1 |
| FLT/Mathlib/RingTheory/Valuation/ValuationSubring.lean | 4 | 0 | 1 |
| FLT/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean | 8 | 0 | 3 |
| FLT/Mathlib/Topology/Algebra/Algebra/Hom.lean | 11 | 1 | 1 |
| FLT/Mathlib/Topology/Algebra/ContinuousAlgEquiv.lean | 1 | 1 | 0 |
| FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean | 6 | 1 | 2 |
| FLT/Mathlib/Topology/Algebra/ContinuousSMulDiscrete.lean | 5 | 0 | 2 |
| FLT/Mathlib/Topology/Algebra/Group/Basic.lean | 3 | 0 | 1 |
| FLT/Mathlib/Topology/Algebra/Group/Quotient.lean | 2 | 0 | 1 |
| FLT/Mathlib/Topology/Algebra/Group/Units.lean | 1 | 0 | 1 |
| FLT/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean | 1 | 0 | 0 |
| FLT/Mathlib/Topology/Algebra/Module/Equiv.lean | 14 | 1 | 3 |
| FLT/Mathlib/Topology/Algebra/Module/FiniteDimension.lean | 1 | 0 | 1 |
| FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean | 33 | 2 | 9 |
| FLT/Mathlib/Topology/Algebra/Module/Quotient.lean | 2 | 0 | 1 |
| FLT/Mathlib/Topology/Algebra/Module/TensorProduct.lean | 7 | 1 | 2 |
| FLT/Mathlib/Topology/Algebra/Monoid.lean | 2 | 0 | 0 |
| FLT/Mathlib/Topology/Algebra/Order/Field.lean | 7 | 1 | 0 |
| FLT/Mathlib/Topology/Algebra/RestrictedProduct/Algebra.lean | 3 | 1 | 0 |
| FLT/Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean | 23 | 0 | 9 |
| FLT/Mathlib/Topology/Algebra/RestrictedProduct/Equiv.lean | 43 | 1 | 5 |
| FLT/Mathlib/Topology/Algebra/RestrictedProduct/Module.lean | 14 | 4 | 1 |
| FLT/Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean | 48 | 4 | 5 |
| FLT/Mathlib/Topology/Algebra/UniformRing.lean | 3 | 0 | 1 |
| FLT/Mathlib/Topology/Algebra/ValuativeRel/ValuativeTopology.lean | 1 | 0 | 0 |
| FLT/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean | 1 | 0 | 1 |
| FLT/Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean | 6 | 1 | 1 |
| FLT/Mathlib/Topology/Bases.lean | 1 | 0 | 1 |
| FLT/Mathlib/Topology/CompactOpen.lean | 1 | 0 | 0 |
| FLT/Mathlib/Topology/Constructions.lean | 3 | 1 | 1 |
| FLT/Mathlib/Topology/HomToDiscrete.lean | 9 | 0 | 1 |
| FLT/Mathlib/Topology/MetricSpace/Pseudo/Matrix.lean | 1 | 0 | 0 |
| FLT/Mathlib/Topology/Polish.lean | 2 | 0 | 2 |
| FLT/NumberField/AdeleRing.lean | 43 | 16 | 2 |
| FLT/NumberField/Completion/Finite.lean | 5 | 2 | 4 |
| FLT/NumberField/Completion/Infinite.lean | 16 | 9 | 0 |
| FLT/NumberField/DiscriminantBounds.lean | 17 | 0 | 0 |
| FLT/NumberField/InfiniteAdeleRing.lean | 7 | 4 | 1 |
| FLT/NumberField/InfinitePlace/Extension.lean | 35 | 0 | 1 |
| FLT/NumberField/Padics/RestrictedProduct.lean | 10 | 1 | 1 |
| FLT/Patching/Algebra.lean | 28 | 3 | 2 |
| FLT/Patching/Module.lean | 48 | 4 | 2 |
| FLT/Patching/Over.lean | 11 | 5 | 1 |
| FLT/Patching/REqualsT.lean | 1 | 1 | 0 |
| FLT/Patching/System.lean | 11 | 6 | 1 |
| FLT/Patching/Ultraproduct.lean | 31 | 3 | 5 |
| FLT/Patching/Utils/AdicTopology.lean | 12 | 0 | 4 |
| FLT/Patching/Utils/CompactHausdorffRings.lean | 4 | 0 | 0 |
| FLT/Patching/Utils/Depth.lean | 13 | 0 | 1 |
| FLT/Patching/Utils/InverseLimit.lean | 3 | 0 | 3 |
| FLT/Patching/Utils/Lemmas.lean | 28 | 0 | 4 |
| FLT/Patching/Utils/StructureFiniteness.lean | 13 | 0 | 1 |
| FLT/Patching/Utils/TopologicallyFG.lean | 2 | 0 | 1 |
| FLT/Patching/VanishingFilter.lean | 11 | 1 | 0 |
| FLT/Proof.lean | 12 | 4 | 1 |
| FLT/QuaternionAlgebra/NumberField.lean | 62 | 6 | 5 |
| FLT/Slop/DimensionTheorem/Defs.lean | 11 | 1 | 4 |
| FLT/Slop/DimensionTheorem/DimEqDelta.lean | 4 | 1 | 1 |
| FLT/Slop/DimensionTheorem/DimLeGrowth.lean | 10 | 2 | 1 |
| FLT/Slop/DimensionTheorem/GrowthLeDelta.lean | 10 | 2 | 1 |
| FLT/Slop/DimensionTheorem/Main.lean | 4 | 4 | 0 |
| FLT/Slop/DimensionTheorem/Numeric.lean | 8 | 0 | 3 |
| FLT/Slop/NumberTheory/TsumDivisorsAntidiagonal.lean | 5 | 0 | 1 |
| FLT/Slop/PGL2/FiniteSubgroups/CyclicPartition.lean | 38 | 1 | 1 |
| FLT/Slop/PGL2/FiniteSubgroups/DicksonClassification.lean | 1 | 3 | 0 |
| FLT/Slop/PGL2/FiniteSubgroups/FieldReconstruction.lean | 96 | 2 | 2 |
| FLT/Slop/PGL2/FiniteSubgroups/NatClassEquation.lean | 7 | 0 | 1 |
| FLT/Slop/PGL2/FiniteSubgroups/PGLBasic.lean | 38 | 1 | 10 |
| FLT/Slop/PGL2/FiniteSubgroups/PSLBasic.lean | 34 | 1 | 1 |
| FLT/Slop/PGL2/FiniteSubgroups/PSLRecognition.lean | 16 | 3 | 1 |
| FLT/Slop/PGL2/FiniteSubgroups/PartitionHelpers.lean | 28 | 1 | 4 |
| FLT/Slop/PGL2/FiniteSubgroups/PartitionProof.lean | 30 | 3 | 1 |
| FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean | 45 | 1 | 2 |
| FLT/Slop/PGL2/FiniteSubgroups/TameClassification.lean | 34 | 3 | 2 |
| FLT/Slop/PGL2/FiniteSubgroups/WildClassification.lean | 25 | 8 | 2 |
| FLT/Slop/RepresentationTheory/OddAbsIrredOrig.lean | 12 | 1 | 0 |
| FLT/Slop/RepresentationTheory/OddAbsIrredSlop.lean | 12 | 0 | 2 |
| FermatsLastTheorem.lean | 1 | 2 | 0 |