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.CanonicalEmbedding): add exists_ne_zero_mem_ringOfIntegers_lt #5650

Closed
wants to merge 67 commits into from
Closed
Changes from 1 commit
Commits
Show all changes
67 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
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
ac06af4
Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb…
xroblot Jul 18, 2023
892e300
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
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
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
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
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
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
b5045fc
Fix names
xroblot Sep 19, 2023
06f8bba
More name fixes
xroblot Sep 19, 2023
bf95cdb
Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi…
xroblot Sep 20, 2023
ad61604
More name changes
xroblot Sep 20, 2023
2a5b356
fix docstring
xroblot Sep 20, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb…
…edding
  • Loading branch information
xroblot committed Jun 28, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit f36170f68dea8b61163fe9246e266c15a410a4c5

This merge commit was added into this branch cleanly.

There are no new changes to show, but you can still view the diff.