FLT/FLT.lean at main · 4hma4d/FLT

Repository navigation

History

100

import FLT.Assumptions.Odlyzko

import FLT.AutomorphicForm.QuaternionAlgebra.Defs

import FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional

import FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract

import FLT.AutomorphicRepresentation.Example

import FLT.Basic.Reductions

import FLT.DedekindDomain.AdicValuation

import FLT.DedekindDomain.FiniteAdeleRing.BaseChange

import FLT.DedekindDomain.FiniteAdeleRing.TensorPi

import FLT.Deformations.Algebra.InverseLimit

import FLT.Deformations.IsResidueAlgebra

import FLT.Deformations.RepresentationTheory.Irreducible

import FLT.Deformations.RepresentationTheory.Subrepresentation

import FLT.DivisionAlgebra.Finiteness

import FLT.EllipticCurve.Torsion

import FLT.GaloisRepresentation.Cyclotomic

import FLT.GaloisRepresentation.HardlyRamified

import FLT.GlobalLanglandsConjectures.GLnDefs

import FLT.GlobalLanglandsConjectures.GLzero

import FLT.GroupScheme.FiniteFlat

import FLT.HIMExperiments.flatness

import FLT.HaarMeasure.DistribHaarChar.Basic

import FLT.HaarMeasure.DistribHaarChar.Padic

import FLT.HaarMeasure.DistribHaarChar.RealComplex

import FLT.HaarMeasure.MeasurableSpacePadics

import FLT.Hard.Results

import FLT.Junk.Algebra

import FLT.Junk.Algebra2

import FLT.Mathlib.Algebra.Algebra.Bilinear

import FLT.Mathlib.Algebra.Algebra.Hom

import FLT.Mathlib.Algebra.Algebra.Pi

import FLT.Mathlib.Algebra.Algebra.Tower

import FLT.Mathlib.Algebra.BigOperators.Group.Finset.Basic

import FLT.Mathlib.Algebra.IsQuaternionAlgebra

import FLT.Mathlib.Algebra.Module.LinearMap.Defs

import FLT.Mathlib.Algebra.Module.Submodule.Basic

import FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic

import FLT.Mathlib.Algebra.Order.GroupWithZero

import FLT.Mathlib.Analysis.Normed.Ring.WithAbs

import FLT.Mathlib.Analysis.SpecialFunctions.Stirling

import FLT.Mathlib.Data.Fin.Basic

import FLT.Mathlib.Data.Set.Card

import FLT.Mathlib.Data.Set.Function

import FLT.Mathlib.GroupTheory.Complement

import FLT.Mathlib.GroupTheory.Index

import FLT.Mathlib.GroupTheory.QuotientGroup.Basic

import FLT.Mathlib.LinearAlgebra.Dimension.Constructions

import FLT.Mathlib.LinearAlgebra.Pi

import FLT.Mathlib.LinearAlgebra.Span.Defs

import FLT.Mathlib.Logic.Equiv.Basic

import FLT.Mathlib.MeasureTheory.Group.Action

import FLT.Mathlib.NumberTheory.NumberField.Basic

import FLT.Mathlib.NumberTheory.NumberField.Completion

import FLT.Mathlib.NumberTheory.Padics.PadicIntegers

import FLT.Mathlib.RepresentationTheory.Basic

import FLT.Mathlib.RingTheory.Finiteness.Pi

import FLT.Mathlib.RingTheory.Ideal.Operations

import FLT.Mathlib.RingTheory.LocalRing.Defs

import FLT.Mathlib.RingTheory.TensorProduct.Basis

import FLT.Mathlib.RingTheory.TensorProduct.Finite

import FLT.Mathlib.RingTheory.TensorProduct.Pi

import FLT.Mathlib.RingTheory.Valuation.ValuationSubring

import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv

import FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom

import FLT.Mathlib.Topology.Algebra.Group.Quotient

import FLT.Mathlib.Topology.Algebra.Module.Equiv

import FLT.Mathlib.Topology.Algebra.Module.FiniteDimension

import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology

import FLT.Mathlib.Topology.Algebra.Module.Quotient

import FLT.Mathlib.Topology.Algebra.Monoid

import FLT.Mathlib.Topology.Algebra.Order.Field

import FLT.Mathlib.Topology.Algebra.UniformRing

import FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology

import FLT.Mathlib.Topology.Algebra.Valued.WithVal

import FLT.Mathlib.Topology.Constructions

import FLT.Mathlib.Topology.Homeomorph

import FLT.Mathlib.Topology.Instances.Matrix

import FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix

import FLT.NumberField.AdeleRing

import FLT.NumberField.Completion.Finite

import FLT.NumberField.Completion.Infinite

import FLT.NumberField.DiscriminantBounds

import FLT.NumberField.Embeddings

import FLT.NumberField.InfiniteAdeleRing

import FLT.NumberField.WeakApproximation

import FLT.Patching.Algebra

import FLT.Patching.Module

import FLT.Patching.Over

import FLT.Patching.REqualsT

import FLT.Patching.System

import FLT.Patching.Ultraproduct

import FLT.Patching.Utils.AdicTopology

import FLT.Patching.Utils.Depth

import FLT.Patching.Utils.InverseLimit

import FLT.Patching.Utils.Lemmas

import FLT.Patching.Utils.StructureFiniteness

import FLT.Patching.Utils.TopologicallyFG

import FLT.Patching.VanishingFilter

import FLT.QuaternionAlgebra.NumberField

import FLT.TateCurve.TateCurve

FilesExpand file tree

FLT.lean

Latest commit

History

FLT.lean

File metadata and controls