|
FLT/Assumptions/KnownIn1980s.lean |
2 |
0 |
|
|
FLT/Assumptions/Mazur.lean |
1 |
0 |
|
|
FLT/Assumptions/Odlyzko.lean |
1 |
0 |
|
|
FLT/AutomorphicForm/QuaternionAlgebra/Defs.lean |
27 |
18 |
|
|
FLT/AutomorphicForm/QuaternionAlgebra/FiniteDimensional.lean |
0 |
1 |
|
|
FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Abstract.lean |
7 |
7 |
|
|
FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean |
15 |
13 |
4 |
|
FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Local.lean |
5 |
14 |
|
|
FLT/Basic/FreyPackage.lean |
7 |
29 |
|
|
FLT/Basic/Reductions.lean |
1 |
4 |
1 |
|
FLT/Data/Hurwitz.lean |
27 |
73 |
|
|
FLT/Data/HurwitzRatHat.lean |
11 |
4 |
4 |
|
FLT/Data/QHat.lean |
15 |
41 |
|
|
FLT/DedekindDomain/AdicValuation.lean |
3 |
30 |
|
|
FLT/DedekindDomain/Completion/BaseChange.lean |
20 |
35 |
|
|
FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean |
22 |
18 |
|
|
FLT/DedekindDomain/FiniteAdeleRing/IsDirectLimitRestricted.lean |
0 |
7 |
|
|
FLT/DedekindDomain/FiniteAdeleRing/LocalUnits.lean |
6 |
5 |
|
|
FLT/DedekindDomain/FiniteAdeleRing/TensorPi.lean |
6 |
3 |
|
|
FLT/DedekindDomain/FiniteAdeleRing/TensorProduct.lean |
2 |
3 |
|
|
FLT/DedekindDomain/FiniteAdeleRing/TensorRestrictedProduct.lean |
5 |
4 |
|
|
FLT/DedekindDomain/IntegralClosure.lean |
5 |
13 |
|
|
FLT/Deformations/Algebra/InverseLimit/Basic.lean |
60 |
26 |
|
|
FLT/Deformations/Algebra/InverseLimit/Topology.lean |
1 |
6 |
|
|
FLT/Deformations/Categories.lean |
22 |
27 |
|
|
FLT/Deformations/ContinuousRepresentation/IsTopologicalModule.lean |
1 |
5 |
|
|
FLT/Deformations/IsProartinian.lean |
1 |
11 |
|
|
FLT/Deformations/IsResidueAlgebra.lean |
3 |
10 |
|
|
FLT/Deformations/Lemmas.lean |
14 |
43 |
|
|
FLT/Deformations/LiftFunctor.lean |
12 |
2 |
|
|
FLT/Deformations/Representable.lean |
4 |
2 |
2 |
|
FLT/Deformations/RepresentationTheory/AbsoluteGaloisGroup.lean |
6 |
14 |
|
|
FLT/Deformations/RepresentationTheory/ContinuousSMulDiscrete.lean |
1 |
6 |
|
|
FLT/Deformations/RepresentationTheory/Etale.lean |
20 |
27 |
|
|
FLT/Deformations/RepresentationTheory/Frobenius.lean |
1 |
4 |
|
|
FLT/Deformations/RepresentationTheory/GaloisRep.lean |
26 |
28 |
|
|
FLT/Deformations/RepresentationTheory/GaloisRepFamily.lean |
2 |
0 |
|
|
FLT/Deformations/RepresentationTheory/IntegralClosure.lean |
5 |
9 |
|
|
FLT/Deformations/RepresentationTheory/Irreducible.lean |
2 |
2 |
|
|
FLT/Deformations/RepresentationTheory/Subrepresentation.lean |
8 |
6 |
|
|
FLT/Deformations/Subfunctor.lean |
10 |
27 |
|
|
FLT/DivisionAlgebra/Finiteness.lean |
42 |
65 |
|
|
FLT/EllipticCurve/Torsion.lean |
6 |
7 |
5 |
|
FLT/GaloisRepresentation/Automorphic.lean |
2 |
3 |
2 |
|
FLT/GaloisRepresentation/Cyclotomic.lean |
2 |
4 |
|
|
FLT/GaloisRepresentation/HardlyRamified/Defs.lean |
3 |
4 |
|
|
FLT/GaloisRepresentation/HardlyRamified/Family.lean |
0 |
1 |
1 |
|
FLT/GaloisRepresentation/HardlyRamified/Frey.lean |
2 |
2 |
2 |
|
FLT/GaloisRepresentation/HardlyRamified/Lift.lean |
0 |
1 |
1 |
|
FLT/GaloisRepresentation/HardlyRamified/ModThree.lean |
0 |
1 |
1 |
|
FLT/GaloisRepresentation/HardlyRamified/Threeadic.lean |
0 |
1 |
1 |
|
FLT/GlobalLanglandsConjectures/GLnDefs.lean |
33 |
18 |
2 |
|
FLT/GlobalLanglandsConjectures/GLzero.lean |
5 |
0 |
1 |
|
FLT/HaarMeasure/HaarChar/AddEquiv.lean |
4 |
26 |
|
|
FLT/HaarMeasure/HaarChar/AdeleRing.lean |
1 |
10 |
|
|
FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean |
13 |
34 |
|
|
FLT/HaarMeasure/HaarChar/FiniteDimensional.lean |
2 |
8 |
|
|
FLT/HaarMeasure/HaarChar/Padic.lean |
0 |
5 |
|
|
FLT/HaarMeasure/HaarChar/RealComplex.lean |
0 |
4 |
|
|
FLT/HaarMeasure/HaarChar/Ring.lean |
4 |
18 |
|
|
FLT/HaarMeasure/MeasurableSpacePadics.lean |
4 |
11 |
|
|
FLT/Hacks/RightActionInstances.lean |
10 |
16 |
|
|
FLT/Mathlib/Algebra/Algebra/Bilinear.lean |
4 |
7 |
|
|
FLT/Mathlib/Algebra/Algebra/Hom.lean |
8 |
14 |
|
|
FLT/Mathlib/Algebra/Algebra/Pi.lean |
3 |
2 |
|
|
FLT/Mathlib/Algebra/Algebra/Tower.lean |
3 |
3 |
|
|
FLT/Mathlib/Algebra/Central/TensorProduct.lean |
0 |
6 |
|
|
FLT/Mathlib/Algebra/FixedPoints/Basic.lean |
10 |
7 |
|
|
FLT/Mathlib/Algebra/IsDirectLimit.lean |
6 |
17 |
|
|
FLT/Mathlib/Algebra/IsQuaternionAlgebra.lean |
2 |
4 |
|
|
FLT/Mathlib/Algebra/Module/LinearMap/Defs.lean |
0 |
1 |
|
|
FLT/Mathlib/Algebra/Module/Submodule/Basic.lean |
1 |
0 |
|
|
FLT/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean |
0 |
13 |
|
|
FLT/Mathlib/Analysis/Normed/Ring/WithAbs.lean |
4 |
10 |
|
|
FLT/Mathlib/Data/Fin/Basic.lean |
0 |
1 |
|
|
FLT/Mathlib/Data/Real/Archimedean.lean |
0 |
2 |
|
|
FLT/Mathlib/Data/Set/Countable.lean |
0 |
1 |
|
|
FLT/Mathlib/Data/Set/Prod.lean |
0 |
1 |
|
|
FLT/Mathlib/GroupTheory/DoubleCoset.lean |
0 |
6 |
|
|
FLT/Mathlib/GroupTheory/Index.lean |
1 |
0 |
|
|
FLT/Mathlib/LinearAlgebra/Countable.lean |
0 |
2 |
|
|
FLT/Mathlib/LinearAlgebra/Determinant.lean |
0 |
11 |
|
|
FLT/Mathlib/LinearAlgebra/Dimension/Constructions.lean |
2 |
1 |
|
|
FLT/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean |
2 |
3 |
|
|
FLT/Mathlib/LinearAlgebra/Matrix/Transvection.lean |
2 |
8 |
|
|
FLT/Mathlib/LinearAlgebra/Pi.lean |
3 |
2 |
|
|
FLT/Mathlib/LinearAlgebra/Span/Defs.lean |
0 |
1 |
|
|
FLT/Mathlib/LinearAlgebra/TensorProduct/Algebra.lean |
1 |
1 |
|
|
FLT/Mathlib/LinearAlgebra/TensorProduct/Basis.lean |
0 |
2 |
|
|
FLT/Mathlib/LinearAlgebra/TensorProduct/FiniteFree.lean |
1 |
0 |
|
|
FLT/Mathlib/MeasureTheory/Constructions/BorelSpace/AdeleRing.lean |
1 |
1 |
|
|
FLT/Mathlib/MeasureTheory/Constructions/BorelSpace/AdicCompletion.lean |
1 |
1 |
|
|
FLT/Mathlib/MeasureTheory/Constructions/BorelSpace/FiniteAdeleRing.lean |
1 |
1 |
|
|
FLT/Mathlib/MeasureTheory/Constructions/BorelSpace/InfinitePlace.lean |
2 |
2 |
|
|
FLT/Mathlib/MeasureTheory/Constructions/BorelSpace/Padic.lean |
1 |
1 |
|
|
FLT/Mathlib/MeasureTheory/Constructions/BorelSpace/RestrictedProduct.lean |
1 |
1 |
|
|
FLT/Mathlib/MeasureTheory/Group/Action.lean |
0 |
18 |
|
|
FLT/Mathlib/MeasureTheory/Group/Measure.lean |
0 |
2 |
|
|
FLT/Mathlib/MeasureTheory/Haar/Extension.lean |
10 |
36 |
|
|
FLT/Mathlib/MeasureTheory/Measure/Regular.lean |
0 |
3 |
|
|
FLT/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean |
0 |
1 |
|
|
FLT/Mathlib/NumberTheory/NumberField/AdeleRing.lean |
0 |
3 |
|
|
FLT/Mathlib/NumberTheory/NumberField/Basic.lean |
0 |
1 |
|
|
FLT/Mathlib/NumberTheory/NumberField/FiniteAdeleRing.lean |
0 |
4 |
|
|
FLT/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean |
4 |
6 |
|
|
FLT/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean |
0 |
1 |
|
|
FLT/Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean |
0 |
2 |
|
|
FLT/Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean |
0 |
13 |
|
|
FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean |
2 |
15 |
|
|
FLT/Mathlib/Order/Filter/Cofinite.lean |
0 |
2 |
|
|
FLT/Mathlib/RepresentationTheory/Basic.lean |
4 |
1 |
|
|
FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean |
0 |
2 |
|
|
FLT/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean |
8 |
7 |
|
|
FLT/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean |
4 |
0 |
|
|
FLT/Mathlib/RingTheory/Ideal/Quotient/Basic.lean |
0 |
1 |
|
|
FLT/Mathlib/RingTheory/LocalRing/Defs.lean |
0 |
2 |
|
|
FLT/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean |
0 |
1 |
|
|
FLT/Mathlib/RingTheory/Localization/BaseChange.lean |
0 |
4 |
|
|
FLT/Mathlib/RingTheory/SimpleRing/TensorProduct.lean |
0 |
8 |
|
|
FLT/Mathlib/RingTheory/TensorProduct/Basis.lean |
1 |
3 |
|
|
FLT/Mathlib/RingTheory/TensorProduct/Pi.lean |
0 |
1 |
|
|
FLT/Mathlib/RingTheory/Valuation/ValuationSubring.lean |
0 |
4 |
|
|
FLT/Mathlib/Topology/Algebra/ContinuousAlgEquiv.lean |
1 |
1 |
|
|
FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean |
7 |
0 |
|
|
FLT/Mathlib/Topology/Algebra/Group/Quotient.lean |
2 |
1 |
|
|
FLT/Mathlib/Topology/Algebra/Group/Units.lean |
0 |
1 |
|
|
FLT/Mathlib/Topology/Algebra/Module/Equiv.lean |
5 |
12 |
|
|
FLT/Mathlib/Topology/Algebra/Module/FiniteDimension.lean |
0 |
1 |
|
|
FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean |
8 |
32 |
|
|
FLT/Mathlib/Topology/Algebra/Module/Quotient.lean |
2 |
0 |
|
|
FLT/Mathlib/Topology/Algebra/Module/TensorProduct.lean |
3 |
4 |
|
|
FLT/Mathlib/Topology/Algebra/Monoid.lean |
0 |
4 |
|
|
FLT/Mathlib/Topology/Algebra/MulAction.lean |
0 |
1 |
|
|
FLT/Mathlib/Topology/Algebra/Order/Field.lean |
0 |
7 |
|
|
FLT/Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean |
13 |
41 |
|
|
FLT/Mathlib/Topology/Algebra/RestrictedProduct/Equiv.lean |
32 |
29 |
|
|
FLT/Mathlib/Topology/Algebra/RestrictedProduct/Module.lean |
6 |
12 |
|
|
FLT/Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean |
19 |
24 |
|
|
FLT/Mathlib/Topology/Algebra/UniformRing.lean |
1 |
2 |
|
|
FLT/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean |
0 |
1 |
|
|
FLT/Mathlib/Topology/Algebra/Valued/WithVal.lean |
2 |
2 |
|
|
FLT/Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean |
0 |
8 |
|
|
FLT/Mathlib/Topology/Bases.lean |
0 |
1 |
|
|
FLT/Mathlib/Topology/Constructions.lean |
0 |
2 |
|
|
FLT/Mathlib/Topology/HomToDiscrete.lean |
0 |
9 |
|
|
FLT/Mathlib/Topology/Homeomorph.lean |
0 |
2 |
|
|
FLT/Mathlib/Topology/Instances/Matrix.lean |
0 |
1 |
|
|
FLT/Mathlib/Topology/MetricSpace/ProperSpace/InfinitePlace.lean |
0 |
1 |
|
|
FLT/Mathlib/Topology/MetricSpace/Pseudo/Matrix.lean |
0 |
1 |
|
|
FLT/Mathlib/Topology/Polish.lean |
0 |
2 |
|
|
FLT/NumberField/AdeleRing.lean |
21 |
29 |
|
|
FLT/NumberField/Completion/Finite.lean |
0 |
8 |
|
|
FLT/NumberField/Completion/Infinite.lean |
10 |
12 |
|
|
FLT/NumberField/DiscriminantBounds.lean |
1 |
7 |
|
|
FLT/NumberField/HeightOneSpectrum.lean |
0 |
2 |
|
|
FLT/NumberField/InfiniteAdeleRing.lean |
7 |
9 |
|
|
FLT/NumberField/InfinitePlace/Dimension.lean |
25 |
47 |
|
|
FLT/NumberField/InfinitePlace/Extension.lean |
14 |
24 |
|
|
FLT/NumberField/InfinitePlace/WeakApproximation.lean |
0 |
11 |
|
|
FLT/NumberField/Padics/RestrictedProduct.lean |
3 |
10 |
|
|
FLT/Patching/Algebra.lean |
16 |
33 |
|
|
FLT/Patching/Module.lean |
28 |
41 |
|
|
FLT/Patching/Over.lean |
7 |
5 |
|
|
FLT/Patching/REqualsT.lean |
0 |
1 |
|
|
FLT/Patching/System.lean |
10 |
12 |
|
|
FLT/Patching/Ultraproduct.lean |
15 |
32 |
|
|
FLT/Patching/Utils/AdicTopology.lean |
2 |
21 |
|
|
FLT/Patching/Utils/Depth.lean |
1 |
13 |
|
|
FLT/Patching/Utils/InverseLimit.lean |
1 |
3 |
|
|
FLT/Patching/Utils/Lemmas.lean |
6 |
29 |
|
|
FLT/Patching/Utils/StructureFiniteness.lean |
22 |
21 |
|
|
FLT/Patching/Utils/TopologicallyFG.lean |
1 |
3 |
|
|
FLT/Patching/VanishingFilter.lean |
3 |
8 |
|
|
FLT/QuaternionAlgebra/NumberField.lean |
10 |
15 |
6 |