FLT/FLT.lean at main · hongjiayang1/FLT

Repository navigation

History

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

import FLT.Assumptions.Mazur

import FLT.Assumptions.Odlyzko

import FLT.AutomorphicForm.QuaternionAlgebra.Defs

import FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional

import FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract

import FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete

import FLT.AutomorphicRepresentation.Example

import FLT.Basic.Reductions

import FLT.DedekindDomain.AdicValuation

import FLT.DedekindDomain.Completion.BaseChange

import FLT.DedekindDomain.FiniteAdeleRing.BaseChange

import FLT.DedekindDomain.FiniteAdeleRing.LocalUnits

import FLT.DedekindDomain.FiniteAdeleRing.TensorPi

import FLT.DedekindDomain.IntegralClosure

import FLT.Deformations.Algebra.InverseLimit.Basic

import FLT.Deformations.Algebra.InverseLimit.Topology

import FLT.Deformations.Categories

import FLT.Deformations.ContinuousRepresentation.IsTopologicalModule

import FLT.Deformations.IsProartinian

import FLT.Deformations.IsResidueAlgebra

import FLT.Deformations.Lemmas

import FLT.Deformations.LiftFunctor

import FLT.Deformations.Representable

import FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup

import FLT.Deformations.RepresentationTheory.Basic

import FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete

import FLT.Deformations.RepresentationTheory.Etale

import FLT.Deformations.RepresentationTheory.Frobenius

import FLT.Deformations.RepresentationTheory.IntegralClosure

import FLT.Deformations.RepresentationTheory.Irreducible

import FLT.Deformations.RepresentationTheory.Subrepresentation

import FLT.Deformations.Subfunctor

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.HaarMeasure.HaarChar.AddEquiv

import FLT.HaarMeasure.HaarChar.AdeleRing

import FLT.HaarMeasure.HaarChar.FiniteDimensional

import FLT.HaarMeasure.HaarChar.Padic

import FLT.HaarMeasure.HaarChar.RealComplex

import FLT.HaarMeasure.HaarChar.Ring

import FLT.HaarMeasure.MeasurableSpacePadics

import FLT.Hacks.RightActionInstances

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.FixedPoints.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.Algebra.Order.GroupWithZero.Canonical

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.Data.Set.Prod

import FLT.Mathlib.GroupTheory.Index

import FLT.Mathlib.GroupTheory.QuotientGroup.Basic

import FLT.Mathlib.LinearAlgebra.Determinant

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.MeasureTheory.Group.Measure

import FLT.Mathlib.MeasureTheory.Measure.OpenPos

import FLT.Mathlib.MeasureTheory.Measure.Regular

import FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite

import FLT.Mathlib.NumberTheory.NumberField.Completion

import FLT.Mathlib.NumberTheory.NumberField.Embeddings

import FLT.Mathlib.NumberTheory.Padics.PadicIntegers

import FLT.Mathlib.NumberTheory.RamificationInertia.Basic

import FLT.Mathlib.RepresentationTheory.Basic

import FLT.Mathlib.RingTheory.Finiteness.Pi

import FLT.Mathlib.RingTheory.Ideal.Quotient.Basic

import FLT.Mathlib.RingTheory.LocalRing.Defs

import FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

import FLT.Mathlib.RingTheory.Localization.BaseChange

import FLT.Mathlib.RingTheory.TensorProduct.Basis

import FLT.Mathlib.RingTheory.TensorProduct.Pi

import FLT.Mathlib.RingTheory.Valuation.ValuationSubring

import FLT.Mathlib.Topology.Algebra.Constructions

import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv

import FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom

import FLT.Mathlib.Topology.Algebra.Group.Basic

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

import FLT.Mathlib.Topology.Algebra.Group.Units

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.MulAction

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

import FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic

import FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module

import FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

import FLT.Mathlib.Topology.Algebra.UniformRing

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

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

import FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt

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.FiniteAdeleRing

import FLT.NumberField.InfiniteAdeleRing

import FLT.NumberField.InfinitePlace.Dimension

import FLT.NumberField.InfinitePlace.Extension

import FLT.NumberField.InfinitePlace.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