Skip to content

Commit 0bf845b

Browse files
riccardobrascariccardobrasca
committed
modulize
1 parent 6989ffe commit 0bf845b

32 files changed

+268
-148
lines changed

‎FltRegular.lean‎

Lines changed: 33 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,33 @@
1-
import FltRegular.CaseI.AuxLemmas
2-
import FltRegular.CaseI.Statement
3-
import FltRegular.CaseII.AuxLemmas
4-
import FltRegular.CaseII.InductionStep
5-
import FltRegular.CaseII.Statement
6-
import FltRegular.FltRegular
7-
import FltRegular.MayAssume.Lemmas
8-
import FltRegular.NumberTheory.Cyclotomic.CaseI
9-
import FltRegular.NumberTheory.Cyclotomic.CyclRat
10-
import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
11-
import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
12-
import FltRegular.NumberTheory.CyclotomicRing
13-
import FltRegular.NumberTheory.Hilbert92
14-
import FltRegular.NumberTheory.Hilbert94
15-
import FltRegular.NumberTheory.KummersLemma.Field
16-
import FltRegular.NumberTheory.KummersLemma.KummersLemma
17-
import FltRegular.NumberTheory.RegularPrimes
18-
import FltRegular.NumberTheory.SystemOfUnits
19-
import FltRegular.NumberTheory.Unramified
20-
import FltRegular.SmallNumbers.Cyclotomic
21-
import FltRegular.SmallNumbers.Eleven.Eleven
22-
import FltRegular.SmallNumbers.Eleven.FLT11
23-
import FltRegular.SmallNumbers.Five.FLT5
24-
import FltRegular.SmallNumbers.Minkowski
25-
import FltRegular.SmallNumbers.OrderOf
26-
import FltRegular.SmallNumbers.PID
27-
import FltRegular.SmallNumbers.Seven.FLT7
28-
import FltRegular.SmallNumbers.Seven.Seven
29-
import FltRegular.SmallNumbers.SmallNumbers
30-
import FltRegular.SmallNumbers.Thirteen.FLT13
31-
import FltRegular.SmallNumbers.Thirteen.Thirteen
1+
module
2+
3+
public import FltRegular.CaseI.AuxLemmas
4+
public import FltRegular.CaseI.Statement
5+
public import FltRegular.CaseII.AuxLemmas
6+
public import FltRegular.CaseII.InductionStep
7+
public import FltRegular.CaseII.Statement
8+
public import FltRegular.FltRegular
9+
public import FltRegular.MayAssume.Lemmas
10+
public import FltRegular.NumberTheory.Cyclotomic.CaseI
11+
public import FltRegular.NumberTheory.Cyclotomic.CyclRat
12+
public import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
13+
public import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
14+
public import FltRegular.NumberTheory.CyclotomicRing
15+
public import FltRegular.NumberTheory.Hilbert92
16+
public import FltRegular.NumberTheory.Hilbert94
17+
public import FltRegular.NumberTheory.KummersLemma.Field
18+
public import FltRegular.NumberTheory.KummersLemma.KummersLemma
19+
public import FltRegular.NumberTheory.RegularPrimes
20+
public import FltRegular.NumberTheory.SystemOfUnits
21+
public import FltRegular.NumberTheory.Unramified
22+
public import FltRegular.SmallNumbers.Cyclotomic
23+
public import FltRegular.SmallNumbers.Eleven.Eleven
24+
public import FltRegular.SmallNumbers.Eleven.FLT11
25+
public import FltRegular.SmallNumbers.Five.FLT5
26+
public import FltRegular.SmallNumbers.Minkowski
27+
public import FltRegular.SmallNumbers.OrderOf
28+
public import FltRegular.SmallNumbers.PID
29+
public import FltRegular.SmallNumbers.Seven.FLT7
30+
public import FltRegular.SmallNumbers.Seven.Seven
31+
public import FltRegular.SmallNumbers.SmallNumbers
32+
public import FltRegular.SmallNumbers.Thirteen.FLT13
33+
public import FltRegular.SmallNumbers.Thirteen.Thirteen

‎FltRegular/CaseI/AuxLemmas.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,8 @@
1-
import FltRegular.NumberTheory.Cyclotomic.CyclRat
1+
module
2+
3+
public import FltRegular.NumberTheory.Cyclotomic.CyclRat
4+
5+
@[expose] public section
26

37
open Finset Nat IsCyclotomicExtension Ideal Polynomial Int Basis
48

‎FltRegular/CaseI/Statement.lean‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,12 @@
1-
import FltRegular.MayAssume.Lemmas
2-
import FltRegular.NumberTheory.Cyclotomic.CaseI
3-
import FltRegular.CaseI.AuxLemmas
4-
import FltRegular.NumberTheory.RegularPrimes
5-
import Mathlib.NumberTheory.FLT.Three
1+
module
2+
3+
public import FltRegular.MayAssume.Lemmas
4+
public import FltRegular.NumberTheory.Cyclotomic.CaseI
5+
public import FltRegular.CaseI.AuxLemmas
6+
public import FltRegular.NumberTheory.RegularPrimes
7+
public import Mathlib.NumberTheory.FLT.Three
8+
9+
@[expose] public section
610

711
open Finset Nat IsCyclotomicExtension Ideal Polynomial Int Basis FltRegular.CaseI
812

‎FltRegular/CaseII/AuxLemmas.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
1-
import Mathlib.RingTheory.ClassGroup
2-
import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
1+
module
2+
3+
public import Mathlib.RingTheory.ClassGroup
4+
public import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
5+
6+
@[expose] public section
37

48
section Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
59

‎FltRegular/CaseII/InductionStep.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
1-
import FltRegular.CaseII.AuxLemmas
2-
import FltRegular.NumberTheory.KummersLemma.KummersLemma
1+
module
2+
3+
public import FltRegular.CaseII.AuxLemmas
4+
public import FltRegular.NumberTheory.KummersLemma.KummersLemma
5+
6+
@[expose] public section
37

48
open scoped nonZeroDivisors NumberField
59
open Polynomial

‎FltRegular/CaseII/Statement.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,8 @@
1-
import FltRegular.CaseII.InductionStep
1+
module
2+
3+
public import FltRegular.CaseII.InductionStep
4+
5+
@[expose] public section
26

37
open scoped nonZeroDivisors NumberField
48
open Polynomial

‎FltRegular/FltRegular.lean‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
1-
import FltRegular.CaseI.Statement
2-
import FltRegular.CaseII.Statement
3-
import Mathlib.NumberTheory.FLT.Basic
1+
module
2+
3+
public import FltRegular.CaseI.Statement
4+
public import FltRegular.CaseII.Statement
5+
public import Mathlib.NumberTheory.FLT.Basic
6+
7+
@[expose] public section
48

59
open FltRegular
610

‎FltRegular/MayAssume/Lemmas.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
1-
import Mathlib.Algebra.GCDMonoid.Finset
2-
import Mathlib.FieldTheory.Finite.Basic
1+
module
2+
3+
public import Mathlib.Algebra.GCDMonoid.Finset
4+
public import Mathlib.FieldTheory.Finite.Basic
5+
6+
@[expose] public section
37

48
open Int Finset
59

‎FltRegular/NumberTheory/Cyclotomic/CaseI.lean‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
1-
import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
2-
import FltRegular.NumberTheory.Cyclotomic.CyclRat
3-
import Mathlib.NumberTheory.NumberField.CMField
1+
module
2+
3+
public import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
4+
public import FltRegular.NumberTheory.Cyclotomic.CyclRat
5+
public import Mathlib.NumberTheory.NumberField.CMField
6+
7+
@[expose] public section
48

59
open scoped NumberField nonZeroDivisors
610

‎FltRegular/NumberTheory/Cyclotomic/CyclRat.lean‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
1-
import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
2-
import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
3-
import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
4-
import Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
5-
import Mathlib.Algebra.CharP.Quotient
6-
import Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
1+
module
2+
3+
public import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
4+
public import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
5+
public import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
6+
public import Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
7+
public import Mathlib.Algebra.CharP.Quotient
8+
public import Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
9+
10+
@[expose] public section
711

812
section Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
913

0 commit comments

Comments
 (0)