Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(NumberTheory.NumberField.Units): proof of Dirichlet's unit theorem #5960

Closed
wants to merge 104 commits into from
Closed
Show file tree
Hide file tree
Changes from 103 commits
Commits
Show all changes
104 commits
Select commit Hold shift + click to select a range
6079e9f
First version
xroblot Jun 27, 2023
f1245a3
Remove unneeded instance
xroblot Jun 27, 2023
f36170f
Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb…
xroblot Jun 28, 2023
a32c2fc
Add mem_span_integralBasis
xroblot Jun 28, 2023
3695a30
Add apply_mem_span_image_iff_mem_span
xroblot Jun 28, 2023
45552e8
Add mem_span_latticeBasis
xroblot Jun 28, 2023
b34f464
Small golf
xroblot Jun 29, 2023
c6c9ddb
Add conj_apply
xroblot Jun 29, 2023
a8f9677
1st commit
xroblot Jul 1, 2023
0695983
Fix line
xroblot Jul 1, 2023
c92dd54
merge
xroblot Jul 1, 2023
7b564c8
Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb…
xroblot Jul 1, 2023
91e8c78
merge
xroblot Jul 1, 2023
047b8c9
Fix backport
xroblot Jul 1, 2023
00c63dc
Move instance
xroblot Jul 2, 2023
00a9038
1st commit
xroblot Jul 2, 2023
d9ec7f1
Merge branch 'xfr-countable_span' into xfr-canonical_embedding_minkowski
xroblot Jul 2, 2023
7ef7609
1st commit
xroblot Jul 5, 2023
3a56308
Add Group.fg_iff_Subgroup_fg
xroblot Jul 5, 2023
fa22093
semicolon
xroblot Jul 6, 2023
de183ff
1st commit
xroblot Jul 6, 2023
993f95a
add results about rootsOfUnity
xroblot Jul 8, 2023
21d7345
Update Zlattice.lean
xroblot Jul 8, 2023
eb432f7
Update Zlattice.lean
xroblot Jul 8, 2023
1a266f6
Update Zlattice.lean
xroblot Jul 8, 2023
95d2fcd
Update Zlattice.lean
xroblot Jul 8, 2023
f999e2e
1st commit
xroblot Jul 17, 2023
07325e1
Update
xroblot Jul 17, 2023
992499e
Merge branch 'xfr-countable_span' into xfr-dirichlet
xroblot Jul 17, 2023
55b67ea
Update
xroblot Jul 18, 2023
c0c771d
Merge branch 'xfr-zlattice_main' into xfr-dirichlet
xroblot Jul 18, 2023
d715893
minimize imports
xroblot Jul 18, 2023
ac06af4
Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb…
xroblot Jul 18, 2023
892e300
update
xroblot Jul 18, 2023
2337643
Merge remote-tracking branch 'origin' into xfr-unit-torsion
xroblot Jul 18, 2023
4a13f86
Update
xroblot Jul 18, 2023
584fc5e
Merge branch 'xfr-refactor_canonical_embedding', remote-tracking bran…
xroblot Jul 19, 2023
b33d146
Update
xroblot Jul 19, 2023
e369851
Merge remote-tracking branch 'origin' into xfr-zlattice_main
xroblot Jul 19, 2023
b9dc461
Merge remote-tracking branch 'origin/xfr-zlattice_main' into xfr-zlat…
xroblot Jul 19, 2023
bc27220
More semicolons
xroblot Jul 19, 2023
045cb4a
Merge branch 'xfr-unit-torsion' into xfr-dirichlet
xroblot Jul 19, 2023
6395d1c
Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet
xroblot Jul 19, 2023
18d3d61
backport
xroblot Jul 19, 2023
a289ca4
Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi…
xroblot Jul 24, 2023
8f6fc4f
1st commit
xroblot Jul 26, 2023
f83eda3
Merge branch 'xfr-refactor_embeddings' into xfr-refactor_canonical_em…
xroblot Jul 28, 2023
0eb1f7f
Merge branch 'xfr-refactor_canonical_embedding' into xfr-canonical_em…
xroblot Jul 28, 2023
1102702
Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet
xroblot Jul 28, 2023
0d22cb8
Merge remote-tracking branch 'origin' into xfr-zlattice_main
xroblot Aug 3, 2023
e794a35
Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb…
xroblot Aug 3, 2023
57728b0
Merge branch 'xfr-refactor_canonical_embedding' into xfr-canonical_em…
xroblot Aug 3, 2023
b8bb31d
Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb…
xroblot Aug 3, 2023
fd620f4
Fix align_import
xroblot Aug 3, 2023
b3030fc
add Finite_bounded_inter_isClosed
xroblot Aug 4, 2023
9bc4c5c
Switch to DiscreteTopology
xroblot Aug 4, 2023
e1bec08
Merge branch 'xfr-refactor_canonical_embedding' into xfr-canonical_em…
xroblot Aug 4, 2023
bfd868e
Line too long
xroblot Aug 4, 2023
ac1e479
Merge branch 'xfr-zlattice_main' into xfr-canonical_embedding_minkowski
xroblot Aug 4, 2023
923f9c9
merge
xroblot Aug 4, 2023
c87e706
Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet
xroblot Aug 4, 2023
0808442
Merge remote-tracking branch 'origin' into xfr-dirichlet
xroblot Aug 8, 2023
3dc3436
add main statements
xroblot Aug 8, 2023
01e244b
1st commit
xroblot Aug 8, 2023
6324f71
Add docs
xroblot Aug 8, 2023
6f2f39b
Add QuotientGroup.mk_prod
xroblot Aug 8, 2023
bcc1b6e
Fix statement
xroblot Aug 8, 2023
cdf26b2
Use DiscreteTopology
xroblot Aug 8, 2023
4114da1
Fix docs
xroblot Aug 8, 2023
dfd08d1
More fixes
xroblot Aug 8, 2023
44a095d
Add the proof of Gershgorin
xroblot Aug 9, 2023
b20a260
review
xroblot Aug 9, 2023
b937109
Merge branch 'xfr-matrix_det_lemma' into xfr-dirichlet
xroblot Aug 9, 2023
2169056
Merge
xroblot Aug 10, 2023
f0f6cbb
Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb…
xroblot Aug 10, 2023
bf2b10e
Docstrings
xroblot Aug 13, 2023
891be93
Merge remote-tracking branch 'origin/xfr-refactor_canonical_embedding…
xroblot Aug 13, 2023
30681d1
Docstring
xroblot Aug 13, 2023
02a0d54
Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi…
xroblot Aug 19, 2023
d20086e
Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet
xroblot Aug 19, 2023
62c5985
fix names
xroblot Aug 20, 2023
ef355cd
Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi…
xroblot Aug 20, 2023
c7bfae6
Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi…
xroblot Aug 24, 2023
f0076cf
typo
xroblot Aug 25, 2023
ed5dff2
1st commit
xroblot Aug 28, 2023
a31dacd
Merge branch 'xfr_complex_measure_ishaar' into xfr-canonical_embeddin…
xroblot Aug 28, 2023
5f48003
Cleanup
xroblot Aug 28, 2023
a0902b4
Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet
xroblot Aug 28, 2023
809f8f1
Merge
xroblot Aug 28, 2023
7e09f65
Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi…
xroblot Sep 1, 2023
3bd156c
Backport
xroblot Sep 1, 2023
629f33b
Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi…
xroblot Sep 16, 2023
1a89daf
Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet
xroblot Sep 16, 2023
433c63e
Clean up after merge
xroblot Sep 16, 2023
a7d7a8f
Update Mathlib/NumberTheory/NumberField/Units.lean
xroblot Sep 16, 2023
3488aff
Merge remote-tracking branch 'origin' into xfr-dirichlet
xroblot Sep 20, 2023
b786b22
Clean up after merge
xroblot Sep 21, 2023
b61a7b7
Review
xroblot Sep 22, 2023
872d1e0
Fix docstrings
xroblot Sep 23, 2023
ae68a0a
new section
xroblot Sep 23, 2023
1020c10
Long line
xroblot Sep 23, 2023
78ce8ff
Review
xroblot Sep 27, 2023
9b6a914
whitespace
xroblot Sep 27, 2023
606d411
Review
xroblot Sep 27, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
5 changes: 5 additions & 0 deletions Mathlib/GroupTheory/QuotientGroup.lean
Original file line number Diff line number Diff line change
Expand Up @@ -191,6 +191,11 @@ theorem mk_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q ) = (a : Q) ^ n :=
#align quotient_group.coe_zpow QuotientGroup.mk_zpow
#align quotient_add_group.coe_zsmul QuotientAddGroup.mk_zsmul

@[to_additive (attr := simp)]
theorem mk_prod {G ι : Type _} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ι → G} :
((Finset.prod s f : G) : G ⧸ N) = Finset.prod s (fun i => (f i : G ⧸ N)) :=
map_prod (QuotientGroup.mk' N) _ _

/-- A group homomorphism `φ : G →* M` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
group homomorphism `G/N →* M`. -/
@[to_additive "An `AddGroup` homomorphism `φ : G →+ M` with `N ⊆ ker(φ)` descends (i.e. `lift`s)
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
Original file line number Diff line number Diff line change
Expand Up @@ -329,7 +329,7 @@ noncomputable abbrev convexBodyLtFactor : ℝ≥0∞ :=
(2 : ℝ≥0∞) ^ card {w : InfinitePlace K // IsReal w} *
volume (ball (0 : ℂ) 1) ^ card {w : InfinitePlace K // IsComplex w}

theorem convexBodyLtFactor_lt_pos : 0 < (convexBodyLtFactor K) := by
theorem convexBodyLtFactor_pos : 0 < (convexBodyLtFactor K) := by
refine mul_pos (NeZero.ne _) ?_
exact ENNReal.pow_ne_zero (ne_of_gt (measure_ball_pos _ _ (by norm_num))) _

Expand Down