-
Notifications
You must be signed in to change notification settings - Fork 55
/
Copy pathFLT.lean
68 lines (68 loc) · 2.94 KB
/
FLT.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
import FLT.AutomorphicForm.QuaternionAlgebra.Defs
import FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional
import FLT.AutomorphicRepresentation.Example
import FLT.Basic.Reductions
import FLT.DedekindDomain.FiniteAdeleRing.BaseChange
import FLT.Deformations.Algebra.InverseLimit
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.DomMulActMeasure
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.Order.AbsoluteValue.Basic
import FLT.Mathlib.Algebra.Order.Hom.Monoid
import FLT.Mathlib.Analysis.Normed.Ring.WithAbs
import FLT.Mathlib.Data.Fin.Basic
import FLT.Mathlib.Data.Finset.Lattice.Fold
import FLT.Mathlib.Data.Set.Card
import FLT.Mathlib.GroupTheory.Complement
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.Span.Defs
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.TensorProduct.Pi
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.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.Constructions
import FLT.Mathlib.Topology.Homeomorph
import FLT.Mathlib.Topology.Instances.Matrix
import FLT.NumberField.AdeleRing
import FLT.NumberField.Completion
import FLT.NumberField.Embeddings
import FLT.NumberField.InfiniteAdeleRing
import FLT.NumberField.WeakApproximation
import FLT.QuaternionAlgebra.NumberField
import FLT.TateCurve.TateCurve