Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

feat(algebra/module/zlattice): prove the characterization of Z-lattices #18477

Closed
wants to merge 154 commits into from
Closed

feat(algebra/module/zlattice): prove the characterization of Z-lattices #18477

wants to merge 154 commits into from

Conversation

xroblot
Copy link
Collaborator

@xroblot xroblot commented Feb 21, 2023 •
edited by github-actions bot
Loading

@xroblot xroblot mentioned this pull request Feb 21, 2023
Closed
3 tasks
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 21, 2023
@xroblot xroblot added WIP Work in progress t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Feb 21, 2023
@xroblot xroblot mentioned this pull request Feb 21, 2023
Closed
4 tasks
xroblot added 15 commits February 21, 2023 18:40
@xroblot xroblot requested a review from a team as a code owner May 5, 2023 15:44
@xroblot xroblot removed the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label May 11, 2023
bors bot pushed a commit that referenced this pull request Jun 9, 2023
@xroblot
feat(algebra/module/zlattice): prove some results about Z-lattices (#…
a3e83f0 
…18266)

For a ℤ-lattice `L` given by `L := submodule.span ℤ (set.range b)` where `b` is a basis of finite dimensional real vector space `E`, this PR defines the fundamental domain of `L` and proves that it is a fundamental domain in the sense of `measure_theory.group.fundamental_domain`. 

It also introduces most of the tools that will be needed to prove that a discrete subgroup of `E` that spans `E` over  `ℝ` is a 
ℤ-lattice, see #18477
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 9, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@xroblot xroblot added the WIP Work in progress label Jun 10, 2023
@github-actions github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jun 24, 2023
@xroblot xroblot added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. and removed WIP Work in progress labels Jun 24, 2023
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 24, 2023
@xroblot xroblot added WIP Work in progress and removed awaiting-review The author would like community review of the PR labels Jul 2, 2023
@xroblot
Copy link
Collaborator Author

xroblot commented Jul 5, 2023

Translated to Mathlib4

@xroblot xroblot closed this Jul 5, 2023
@YaelDillies YaelDillies deleted the xfr-zlattice_theory branch November 18, 2023 11:26
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
Labels
modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. t-number-theory Number theory (also use t-algebra or t-analysis to specialize) WIP Work in progress
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@xroblot @mathlib-dependent-issues-bot @eric-wieser @hrmacbeth @urkud