FLT.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 260 imports below, so a file that imports it gets all of them.
Imports
- FLT.Assumptions.KnownIn1980s
- FLT.Assumptions.Mazur
- FLT.Assumptions.Odlyzko
- FLT.AutomorphicForm.GroupTheoryStuff
- FLT.AutomorphicForm.QuaternionAlgebra.Basic
- FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional
- FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract
- FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete
- FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local
- FLT.AutomorphicForm.QuaternionAlgebra.InnerProduct
- FLT.AutomorphicForm.Stuff
- FLT.Basic.Lemmas
- FLT.Data.Hurwitz
- FLT.Data.HurwitzRatHat
- FLT.Data.QHat
- FLT.DedekindDomain.AdicValuation
- FLT.DedekindDomain.Completion.BaseChange
- FLT.DedekindDomain.FiniteAdeleRing.BaseChange
- FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted
- FLT.DedekindDomain.FiniteAdeleRing.LocalUnits
- FLT.DedekindDomain.FiniteAdeleRing.TensorPi
- FLT.DedekindDomain.FiniteAdeleRing.TensorProduct
- FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct
- FLT.DedekindDomain.IntegralClosure
- FLT.Deformations.Algebra.InverseLimit.Basic
- FLT.Deformations.Algebra.InverseLimit.Topology
- FLT.Deformations.Categories
- FLT.Deformations.ContinuousRepresentation.IsTopologicalModule
- FLT.Deformations.IsProartinian
- FLT.Deformations.IsResidueAlgebra
- FLT.Deformations.Lemmas
- FLT.Deformations.LiftFunctor
- FLT.Deformations.Representable
- FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup
- FLT.Deformations.RepresentationTheory.Etale
- FLT.Deformations.RepresentationTheory.Frobenius
- FLT.Deformations.RepresentationTheory.GaloisRep
- FLT.Deformations.RepresentationTheory.GaloisRepFamily
- FLT.Deformations.RepresentationTheory.IntegralClosure
- FLT.Deformations.RepresentationTheory.Irreducible
- FLT.Deformations.Subfunctor
- FLT.DivisionAlgebra.Finiteness
- FLT.EllipticCurve.Torsion
- FLT.FreyCurve.Basic
- FLT.FreyCurve.FreyPackage
- FLT.FreyCurve.Mazur
- FLT.GaloisRepresentation.Automorphic
- FLT.GaloisRepresentation.Cyclotomic
- FLT.GaloisRepresentation.HardlyRamified.Defs
- FLT.GaloisRepresentation.HardlyRamified.Family
- FLT.GaloisRepresentation.HardlyRamified.Frey
- FLT.GaloisRepresentation.HardlyRamified.Lift
- FLT.GaloisRepresentation.HardlyRamified.ModThree
- FLT.GaloisRepresentation.HardlyRamified.Threeadic
- FLT.GlobalLanglandsConjectures.GLnDefs
- FLT.GlobalLanglandsConjectures.GLzero
- FLT.GroupScheme.FiniteFlat
- FLT.HaarMeasure.FiniteAdeleRing
- FLT.HaarMeasure.HaarChar.AddEquiv
- FLT.HaarMeasure.HaarChar.AdeleRing
- FLT.HaarMeasure.HaarChar.FiniteAdeleRing
- FLT.HaarMeasure.HaarChar.FiniteDimensional
- FLT.HaarMeasure.HaarChar.Padic
- FLT.HaarMeasure.HaarChar.RealComplex
- FLT.HaarMeasure.HaarChar.Ring
- FLT.HaarMeasure.MeasurableSpacePadics
- FLT.HaarMeasure.Quotient
- FLT.Hacks.RightActionInstances
- FLT.HenselianLocalRing.EtaleDecomposition
- FLT.HenselianLocalRing.Finite
- FLT.HenselianLocalRing.Stuff
- FLT.KnownIn1980s.EllipticCurves.Flat
- FLT.KnownIn1980s.EllipticCurves.GoodReduction
- FLT.KnownIn1980s.EllipticCurves.QuadraticTwists.QuadraticTwists
- FLT.KnownIn1980s.EllipticCurves.QuadraticTwists.SplitMultiplicativeReduction
- FLT.KnownIn1980s.EllipticCurves.ReductionBaseChange
- FLT.KnownIn1980s.EllipticCurves.TateCurve
- FLT.KnownIn1980s.EllipticCurves.TateCurveBaseChange
- FLT.KnownIn1980s.EllipticCurves.TateCurveConstruction
- FLT.KnownIn1980s.EllipticCurves.TateParameter
- FLT.KnownIn1980s.EllipticCurves.Torsion
- FLT.KnownIn1980s.EllipticCurves.WeilPairing
- FLT.KnownIn1980s.PGL2.Defs
- FLT.KnownIn1980s.PGL2.Proofs
- FLT.KnownIn1980s.RepresentationTheory.OddAbsIrred
- FLT.Mathlib.Algebra.Algebra.Bilinear
- FLT.Mathlib.Algebra.Algebra.Equiv
- FLT.Mathlib.Algebra.Algebra.Hom
- FLT.Mathlib.Algebra.Algebra.Pi
- FLT.Mathlib.Algebra.Algebra.Tower
- FLT.Mathlib.Algebra.Category.ModuleCat.Topology.Basic
- FLT.Mathlib.Algebra.Category.ModuleCat.Topology.Homology
- FLT.Mathlib.Algebra.Central.TensorProduct
- FLT.Mathlib.Algebra.FixedPoints.Basic
- FLT.Mathlib.Algebra.Group.Action.Hom
- FLT.Mathlib.Algebra.Homology.HomologicalComplex
- FLT.Mathlib.Algebra.IsDirectLimit
- FLT.Mathlib.Algebra.IsQuaternionAlgebra
- FLT.Mathlib.Algebra.Module.Submodule.Basic
- FLT.Mathlib.Algebra.Module.TransferInstance
- FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic
- FLT.Mathlib.Algebra.Polynomial.QuadraticDiscriminant
- FLT.Mathlib.Algebra.Polynomial.Splits
- FLT.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
- FLT.Mathlib.AlgebraicGeometry.EllipticCurve.Aut
- FLT.Mathlib.AlgebraicGeometry.EllipticCurve.GaloisDescent
- FLT.Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
- FLT.Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
- FLT.Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
- FLT.Mathlib.Analysis.Normed.Ring.WithAbs
- FLT.Mathlib.Data.Fin.Basic
- FLT.Mathlib.Data.Real.Archimedean
- FLT.Mathlib.Data.Set.Prod
- FLT.Mathlib.FieldTheory.Galois.Basic
- FLT.Mathlib.FieldTheory.Galois.Infinite
- FLT.Mathlib.FieldTheory.Separable
- FLT.Mathlib.FieldTheory.SeparableDegree
- FLT.Mathlib.FieldTheory.SplittingField.IsSplittingField
- FLT.Mathlib.GroupTheory.DoubleCoset
- FLT.Mathlib.GroupTheory.GroupAction.Quotient
- FLT.Mathlib.GroupTheory.Index
- FLT.Mathlib.GroupTheory.SpecificGroups.Cyclic
- FLT.Mathlib.LinearAlgebra.Countable
- FLT.Mathlib.LinearAlgebra.Determinant
- FLT.Mathlib.LinearAlgebra.Dimension.Constructions
- FLT.Mathlib.LinearAlgebra.Dimension.IsQuadraticExtension
- FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
- FLT.Mathlib.LinearAlgebra.Matrix.Transvection
- FLT.Mathlib.LinearAlgebra.Pi
- FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra
- FLT.Mathlib.LinearAlgebra.TensorProduct.Basis
- FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree
- FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing
- FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion
- FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing
- FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace
- FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic
- FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct
- FLT.Mathlib.MeasureTheory.Group.Action
- FLT.Mathlib.MeasureTheory.Group.Measure
- FLT.Mathlib.MeasureTheory.Group.ModularCharacter
- FLT.Mathlib.MeasureTheory.Haar.Extension
- FLT.Mathlib.MeasureTheory.Measure.Regular
- FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite
- FLT.Mathlib.NumberTheory.NumberField.AdeleRing
- FLT.Mathlib.NumberTheory.NumberField.Completion
- FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing
- FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
- FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
- FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion
- FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum
- FLT.Mathlib.NumberTheory.Padics.PadicIntegers
- FLT.Mathlib.Order.Filter.Cofinite
- FLT.Mathlib.RepresentationTheory.Basic
- FLT.Mathlib.RepresentationTheory.Continuous.Basic
- FLT.Mathlib.RepresentationTheory.Continuous.TopRep
- FLT.Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
- FLT.Mathlib.RepresentationTheory.Homological.ContCohomology.CupProduct
- FLT.Mathlib.RingTheory.AdjoinRoot
- FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation
- FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
- FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
- FLT.Mathlib.RingTheory.DiscreteValuationRing.AdjoinRoot
- FLT.Mathlib.RingTheory.DiscreteValuationRing.Separable
- FLT.Mathlib.RingTheory.Ideal.Quotient.Basic
- FLT.Mathlib.RingTheory.LocalRing.Defs
- FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
- FLT.Mathlib.RingTheory.Localization.BaseChange
- FLT.Mathlib.RingTheory.Norm.Quadratic
- FLT.Mathlib.RingTheory.Norm.Quotient
- FLT.Mathlib.RingTheory.Polynomial.GaussLemma
- FLT.Mathlib.RingTheory.RamificationInertia.Basic
- FLT.Mathlib.RingTheory.SimpleRing.TensorProduct
- FLT.Mathlib.RingTheory.TensorProduct.Basis
- FLT.Mathlib.RingTheory.TensorProduct.Pi
- FLT.Mathlib.RingTheory.Unramified.LocalRing
- FLT.Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
- FLT.Mathlib.RingTheory.Valuation.ValuationSubring
- FLT.Mathlib.RingTheory.Valuation.ValuativeRel.Basic
- FLT.Mathlib.Topology.Algebra.Algebra.Hom
- FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
- FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom
- FLT.Mathlib.Topology.Algebra.ContinuousSMulDiscrete
- FLT.Mathlib.Topology.Algebra.Group.Basic
- FLT.Mathlib.Topology.Algebra.Group.Quotient
- FLT.Mathlib.Topology.Algebra.Group.Units
- FLT.Mathlib.Topology.Algebra.IsUniformGroup.Basic
- FLT.Mathlib.Topology.Algebra.Module.CompactOpen
- FLT.Mathlib.Topology.Algebra.Module.Equiv
- FLT.Mathlib.Topology.Algebra.Module.FiniteDimension
- FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
- FLT.Mathlib.Topology.Algebra.Module.Quotient
- FLT.Mathlib.Topology.Algebra.Module.TensorProduct
- FLT.Mathlib.Topology.Algebra.Monoid
- FLT.Mathlib.Topology.Algebra.MulAction
- FLT.Mathlib.Topology.Algebra.Order.Field
- FLT.Mathlib.Topology.Algebra.RestrictedProduct.Algebra
- FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic
- FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv
- FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module
- FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
- FLT.Mathlib.Topology.Algebra.UniformRing
- FLT.Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
- FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology
- FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt
- FLT.Mathlib.Topology.Bases
- FLT.Mathlib.Topology.CompactOpen
- FLT.Mathlib.Topology.Constructions
- FLT.Mathlib.Topology.HomToDiscrete
- FLT.Mathlib.Topology.Instances.Matrix
- FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace
- FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix
- FLT.Mathlib.Topology.Polish
- FLT.NumberField.AdeleRing
- FLT.NumberField.Completion.Finite
- FLT.NumberField.Completion.Infinite
- FLT.NumberField.DiscriminantBounds
- FLT.NumberField.HeightOneSpectrum
- FLT.NumberField.InfiniteAdeleRing
- FLT.NumberField.InfinitePlace.Extension
- FLT.NumberField.Padics.RestrictedProduct
- FLT.Patching.Algebra
- FLT.Patching.Module
- FLT.Patching.Over
- FLT.Patching.REqualsT
- FLT.Patching.System
- FLT.Patching.Ultraproduct
- FLT.Patching.Utils.AdicTopology
- FLT.Patching.Utils.CompactHausdorffRings
- FLT.Patching.Utils.Depth
- FLT.Patching.Utils.InverseLimit
- FLT.Patching.Utils.Lemmas
- FLT.Patching.Utils.StructureFiniteness
- FLT.Patching.Utils.TopologicallyFG
- FLT.Patching.VanishingFilter
- FLT.Proof
- FLT.QuaternionAlgebra.NumberField
- FLT.Slop.DimensionTheorem
- FLT.Slop.DimensionTheorem.Defs
- FLT.Slop.DimensionTheorem.DimEqDelta
- FLT.Slop.DimensionTheorem.DimLeGrowth
- FLT.Slop.DimensionTheorem.GrowthLeDelta
- FLT.Slop.DimensionTheorem.Main
- FLT.Slop.DimensionTheorem.Numeric
- FLT.Slop.NumberTheory.TsumDivisorsAntidiagonal
- FLT.Slop.PGL2.FiniteSubgroups.CyclicPartition
- FLT.Slop.PGL2.FiniteSubgroups.DicksonClassification
- FLT.Slop.PGL2.FiniteSubgroups.FieldReconstruction
- FLT.Slop.PGL2.FiniteSubgroups.NatClassEquation
- FLT.Slop.PGL2.FiniteSubgroups.PGLBasic
- FLT.Slop.PGL2.FiniteSubgroups.PSLBasic
- FLT.Slop.PGL2.FiniteSubgroups.PSLRecognition
- FLT.Slop.PGL2.FiniteSubgroups.PartitionHelpers
- FLT.Slop.PGL2.FiniteSubgroups.PartitionProof
- FLT.Slop.PGL2.FiniteSubgroups.RecognitionA5
- FLT.Slop.PGL2.FiniteSubgroups.TameClassification
- FLT.Slop.PGL2.FiniteSubgroups.WildClassification
- FLT.Slop.RepresentationTheory.OddAbsIrredOrig
- FLT.Slop.RepresentationTheory.OddAbsIrredSlop
- FLT.TateCurve.TateCurve