Documentation
FLT
Search
return to top
source
Imports
Init
FLT.AutomorphicRepresentation.Example
FLT.Basic.Reductions
FLT.Deformations.IsResidueAlgebra
FLT.DivisionAlgebra.Finiteness
FLT.EllipticCurve.Torsion
FLT.GaloisRepresentation.Cyclotomic
FLT.GaloisRepresentation.HardlyRamified
FLT.GlobalLanglandsConjectures.GLnDefs
FLT.GlobalLanglandsConjectures.GLzero
FLT.GroupScheme.FiniteFlat
FLT.HIMExperiments.flatness
FLT.HaarMeasure.MeasurableSpacePadics
FLT.Hard.Results
FLT.Junk.Algebra
FLT.Junk.Algebra2
FLT.NumberField.AdeleRing
FLT.NumberField.Completion
FLT.NumberField.Embeddings
FLT.NumberField.InfiniteAdeleRing
FLT.NumberField.WeakApproximation
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.TateCurve.TateCurve
FLT.AutomorphicForm.QuaternionAlgebra.Defs
FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional
FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators
FLT.DedekindDomain.FiniteAdeleRing.BaseChange
FLT.DedekindDomain.FiniteAdeleRing.TensorPi
FLT.Deformations.Algebra.InverseLimit
FLT.Deformations.RepresentationTheory.Irreducible
FLT.Deformations.RepresentationTheory.Subrepresentation
FLT.HaarMeasure.DistribHaarChar.Basic
FLT.HaarMeasure.DistribHaarChar.Padic
FLT.HaarMeasure.DistribHaarChar.RealComplex
FLT.Mathlib.Algebra.IsQuaternionAlgebra
FLT.Mathlib.GroupTheory.Complement
FLT.Mathlib.GroupTheory.Index
FLT.Mathlib.RepresentationTheory.Basic
FLT.Mathlib.Topology.Constructions
FLT.Mathlib.Topology.Homeomorph
FLT.Patching.Utils.AdicTopology
FLT.Patching.Utils.Depth
FLT.Patching.Utils.InverseLimit
FLT.Patching.Utils.Lemmas
FLT.Patching.Utils.StructureFiniteness
FLT.Patching.Utils.TopologicallyFG
FLT.Mathlib.Algebra.Algebra.Bilinear
FLT.Mathlib.Algebra.Algebra.Hom
FLT.Mathlib.Algebra.Algebra.Pi
FLT.Mathlib.Algebra.Algebra.Tower
FLT.Mathlib.Data.Fin.Basic
FLT.Mathlib.Data.Set.Card
FLT.Mathlib.Data.Set.Function
FLT.Mathlib.GroupTheory.QuotientGroup.Basic
FLT.Mathlib.LinearAlgebra.Dimension.Constructions
FLT.Mathlib.LinearAlgebra.Span.Defs
FLT.Mathlib.MeasureTheory.Group.Action
FLT.Mathlib.NumberTheory.NumberField.Basic
FLT.Mathlib.NumberTheory.NumberField.Completion
FLT.Mathlib.NumberTheory.Padics.PadicIntegers
FLT.Mathlib.RingTheory.LocalRing.Defs
FLT.Mathlib.RingTheory.TensorProduct.Finite
FLT.Mathlib.RingTheory.TensorProduct.Pi
FLT.Mathlib.RingTheory.Valuation.ValuationSubring
FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom
FLT.Mathlib.Topology.Algebra.Monoid
FLT.Mathlib.Topology.Algebra.UniformRing
FLT.Mathlib.Topology.Instances.Matrix
FLT.Mathlib.Algebra.Module.LinearMap.Defs
FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic
FLT.Mathlib.Algebra.Order.Hom.Monoid
FLT.Mathlib.Analysis.Normed.Ring.WithAbs
FLT.Mathlib.Topology.Algebra.Group.Quotient
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.Order.Field
FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology
FLT.Mathlib.Topology.Algebra.Valued.WithVal
FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix
FLT.Mathlib.Algebra.BigOperators.Group.Finset.Basic
Imported by