-
Notifications
You must be signed in to change notification settings - Fork 1
/
FltRegular.lean
31 lines (31 loc) · 1.32 KB
/
FltRegular.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
import FltRegular.CaseI.AuxLemmas
import FltRegular.CaseI.Statement
import FltRegular.CaseII.AuxLemmas
import FltRegular.CaseII.InductionStep
import FltRegular.CaseII.Statement
import FltRegular.FLT5
import FltRegular.FltRegular
import FltRegular.MayAssume.Lemmas
import FltRegular.NumberTheory.AuxLemmas
import FltRegular.NumberTheory.Cyclotomic.CaseI
import FltRegular.NumberTheory.Cyclotomic.CyclRat
import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
import FltRegular.NumberTheory.Cyclotomic.Factoring
import FltRegular.NumberTheory.Cyclotomic.GaloisActionOnCyclo
import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
import FltRegular.NumberTheory.CyclotomicRing
import FltRegular.NumberTheory.Different
import FltRegular.NumberTheory.Finrank
import FltRegular.NumberTheory.GaloisPrime
import FltRegular.NumberTheory.Hilbert90
import FltRegular.NumberTheory.Hilbert92
import FltRegular.NumberTheory.Hilbert94
import FltRegular.NumberTheory.IdealNorm
import FltRegular.NumberTheory.KummersLemma.Field
import FltRegular.NumberTheory.KummersLemma.KummersLemma
import FltRegular.NumberTheory.QuotientTrace
import FltRegular.NumberTheory.RegularPrimes
import FltRegular.NumberTheory.SystemOfUnits
import FltRegular.NumberTheory.Unramified
import FltRegular.ReadyForMathlib.Homogenization