Documentation
FLT
Search
return to top
source
Imports
Init
FLT.Proof
FLT.Assumptions.KnownIn1980s
FLT.Assumptions.Mazur
FLT.Assumptions.Odlyzko
FLT.AutomorphicForm.GroupTheoryStuff
FLT.AutomorphicForm.Stuff
FLT.Basic.Lemmas
FLT.Data.Hurwitz
FLT.Data.HurwitzRatHat
FLT.Data.QHat
FLT.DedekindDomain.AdicValuation
FLT.DedekindDomain.IntegralClosure
FLT.Deformations.Categories
FLT.Deformations.IsProartinian
FLT.Deformations.IsResidueAlgebra
FLT.Deformations.Lemmas
FLT.Deformations.LiftFunctor
FLT.Deformations.Representable
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.GlobalLanglandsConjectures.GLnDefs
FLT.GlobalLanglandsConjectures.GLzero
FLT.GroupScheme.FiniteFlat
FLT.HaarMeasure.FiniteAdeleRing
FLT.HaarMeasure.MeasurableSpacePadics
FLT.HaarMeasure.Quotient
FLT.Hacks.RightActionInstances
FLT.HenselianLocalRing.EtaleDecomposition
FLT.HenselianLocalRing.Finite
FLT.HenselianLocalRing.Stuff
FLT.NumberField.AdeleRing
FLT.NumberField.DiscriminantBounds
FLT.NumberField.HeightOneSpectrum
FLT.NumberField.InfiniteAdeleRing
FLT.Patching.Algebra
FLT.Patching.Module
FLT.Patching.Over
FLT.Patching.REqualsT
FLT.Patching.System
FLT.Patching.Ultraproduct
FLT.Patching.VanishingFilter
FLT.QuaternionAlgebra.NumberField
FLT.Slop.DimensionTheorem
FLT.TateCurve.TateCurve
FLT.AutomorphicForm.QuaternionAlgebra.Basic
FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional
FLT.AutomorphicForm.QuaternionAlgebra.InnerProduct
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.Deformations.ContinuousRepresentation.IsTopologicalModule
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.GaloisRepresentation.HardlyRamified.Defs
FLT.GaloisRepresentation.HardlyRamified.Family
FLT.GaloisRepresentation.HardlyRamified.Frey
FLT.GaloisRepresentation.HardlyRamified.Lift
FLT.GaloisRepresentation.HardlyRamified.ModThree
FLT.GaloisRepresentation.HardlyRamified.Threeadic
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.KnownIn1980s.EllipticCurves.Flat
FLT.KnownIn1980s.EllipticCurves.GoodReduction
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.IsDirectLimit
FLT.Mathlib.Algebra.IsQuaternionAlgebra
FLT.Mathlib.FieldTheory.Separable
FLT.Mathlib.FieldTheory.SeparableDegree
FLT.Mathlib.GroupTheory.DoubleCoset
FLT.Mathlib.GroupTheory.Index
FLT.Mathlib.LinearAlgebra.Countable
FLT.Mathlib.LinearAlgebra.Determinant
FLT.Mathlib.LinearAlgebra.Pi
FLT.Mathlib.RepresentationTheory.Basic
FLT.Mathlib.RingTheory.AdjoinRoot
FLT.Mathlib.Topology.Bases
FLT.Mathlib.Topology.CompactOpen
FLT.Mathlib.Topology.Constructions
FLT.Mathlib.Topology.HomToDiscrete
FLT.Mathlib.Topology.Polish
FLT.NumberField.Completion.Finite
FLT.NumberField.Completion.Infinite
FLT.NumberField.InfinitePlace.Extension
FLT.NumberField.Padics.RestrictedProduct
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.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.RepresentationTheory.OddAbsIrredOrig
FLT.Slop.RepresentationTheory.OddAbsIrredSlop
FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract
FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete
FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local
FLT.Deformations.Algebra.InverseLimit.Basic
FLT.Deformations.Algebra.InverseLimit.Topology
FLT.KnownIn1980s.EllipticCurves.QuadraticTwists.QuadraticTwists
FLT.KnownIn1980s.EllipticCurves.QuadraticTwists.SplitMultiplicativeReduction
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.Central.TensorProduct
FLT.Mathlib.Algebra.FixedPoints.Basic
FLT.Mathlib.Algebra.Homology.HomologicalComplex
FLT.Mathlib.Algebra.Module.TransferInstance
FLT.Mathlib.Algebra.Polynomial.QuadraticDiscriminant
FLT.Mathlib.Algebra.Polynomial.Splits
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.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.SplittingField.IsSplittingField
FLT.Mathlib.GroupTheory.GroupAction.Quotient
FLT.Mathlib.GroupTheory.SpecificGroups.Cyclic
FLT.Mathlib.LinearAlgebra.Dimension.Constructions
FLT.Mathlib.LinearAlgebra.Dimension.IsQuadraticExtension
FLT.Mathlib.LinearAlgebra.Matrix.Transvection
FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra
FLT.Mathlib.LinearAlgebra.TensorProduct.Basis
FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree
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.NumberTheory.NumberField.AdeleRing
FLT.Mathlib.NumberTheory.NumberField.Completion
FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing
FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum
FLT.Mathlib.NumberTheory.Padics.PadicIntegers
FLT.Mathlib.Order.Filter.Cofinite
FLT.Mathlib.RepresentationTheory.Continuous.Basic
FLT.Mathlib.RepresentationTheory.Continuous.TopRep
FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation
FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
FLT.Mathlib.RingTheory.DiscreteValuationRing.AdjoinRoot
FLT.Mathlib.RingTheory.DiscreteValuationRing.Separable
FLT.Mathlib.RingTheory.LocalRing.Defs
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.ValuationSubring
FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom
FLT.Mathlib.Topology.Algebra.ContinuousSMulDiscrete
FLT.Mathlib.Topology.Algebra.Monoid
FLT.Mathlib.Topology.Algebra.MulAction
FLT.Mathlib.Topology.Algebra.UniformRing
FLT.Mathlib.Topology.Instances.Matrix
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.Mathlib.Algebra.Group.Action.Hom
FLT.Mathlib.Algebra.Module.Submodule.Basic
FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic
FLT.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
FLT.Mathlib.Analysis.Normed.Ring.WithAbs
FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
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.Measure.Typeclasses.Finite
FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion
FLT.Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
FLT.Mathlib.RepresentationTheory.Homological.ContCohomology.CupProduct
FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
FLT.Mathlib.RingTheory.Ideal.Quotient.Basic
FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
FLT.Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
FLT.Mathlib.RingTheory.Valuation.ValuativeRel.Basic
FLT.Mathlib.Topology.Algebra.Algebra.Hom
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.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.ValuativeRel.ValuativeTopology
FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology
FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt
FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace
FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix
FLT.Mathlib.Algebra.Category.ModuleCat.Topology.Basic
FLT.Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Imported by