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.

Sign up for GitHub

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

Jump to bottom

feat(analysis/normed_space/lattice_ordered_group): Lattice ordered group lemmas #9548

Closed
wants to merge 38 commits into from
Closed

feat(analysis/normed_space/lattice_ordered_group): Lattice ordered group lemmas #9548

wants to merge 38 commits into from

Conversation

mans0954
Copy link
Collaborator

@mans0954 mans0954 commented Oct 4, 2021 •
edited by github-actions bot

Adds some useful lattice ordered group lemmas, needed by #10322.

Open in Gitpod

mans0954 and others added 7 commits October 5, 2021 18:30
@mans0954 @eric-wieser
Spacing
f178c67 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mans0954 @eric-wieser
Whitespace
080a1b1 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mans0954 @eric-wieser
Whitespace
33f9629 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mans0954 @eric-wieser
Remove label
8385a06 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mans0954 @eric-wieser
Remove by exact
70745c6 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mans0954
Fix docstrings
c7aa7cd
@mans0954
Include multiplicative docstrings for definitions
72ced73
@mans0954 mans0954 added the awaiting-review The author would like community review of the PR label Oct 6, 2021
@ocfnash
Copy link
Collaborator

ocfnash commented Nov 22, 2021

Thank you for this PR @mans0954 and thank you for your patience with this PR.

I'm sorry that this proposal has been open for so long without resolution so I've just taken a careful look to see what we can do. It looks to me like there are four things happening here:

  1. Introducing classes has_pos_part, has_neg_part and associating these with the postfix notation ⁺, ⁻ instead of mpos and mneg.
  2. Changing many comments in src/algebra/lattice_ordered_group.lean
  3. Adding some new lemmas e.g., abs_abs_div_abs_le, two_inf_sub_two_inf_le etc.
  4. Making changes to very fundamental stuff like introducing a multiplicative version of sub_add_cancel except it has to be called div_mul_cancel' rather than div_mul_cancel because the latter is already taken for a group_with_zero rather than a plain group.

Do you think you would be able to split it up, into several PRs, perhaps (but not necessarily) along the lines above so that it is easier to focus on each of the various changes?

Though the various pieces are related, each of them is likely to need discussion in its own right.

@ocfnash ocfnash added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Nov 22, 2021
@mans0954
Copy link
Collaborator Author

Do you think you would be able to split it up, into several PRs, perhaps (but not necessarily) along the lines above so that it is easier to focus on each of the various changes?

I could do that it it would help? 1) and 2) were the outcome of previous review of this PR #9548 (review) #9548 (review) and 4) is motivated by feedback on a previous PR #8663 (review) and #8673 (comment) .

The impact of changes 1) and 2) is limited to code I wrote in my recent PRs #8673, #9172, #9274, which, together with this PR are building towards #10322.

@mans0954 mans0954 mentioned this pull request Nov 22, 2021
Closed
@github-actions github-actions 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 Nov 22, 2021
@mans0954 mans0954 mentioned this pull request Nov 22, 2021
Closed
bors bot pushed a commit that referenced this pull request Nov 23, 2021
@mans0954
refactor(algebra.group.basic): Convert sub_add_cancel and neg_sub to …
2b75493 
…multaplicative form (#10419)

Currently mathlib has a rich set of lemmas connecting the addition, subtraction and negation additive group operations, but a far thinner collection of results for multiplication, division and inverse multiplicative group operations, despite the fact that the former can be generated easily from the latter via `to_additive`.

In  #9548 I require multiplicative forms of the existing `sub_add_cancel` and `neg_sub` lemmas. This PR refactors them as the equivalent multiplicative results and then recovers `sub_add_cancel` and `neg_sub` via `to_additive`. There is a complication in that unfortunately `group_with_zero` already has lemmas named `inv_div` and `div_mul_cancel`. I have worked around this by naming the lemmas in this PR `inv_div'` and `div_mul_cancel'` and then manually overriding the names generated by `to_additive`. Other suggestions as to how to approach this welcome.
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Nov 24, 2021
@github-actions
Copy link

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 24, 2021
ericrbg pushed a commit that referenced this pull request Nov 24, 2021
@mans0954 @ericrbg
refactor(algebra.group.basic): Convert sub_add_cancel and neg_sub to …
354f2d6 
…multaplicative form (#10419)

Currently mathlib has a rich set of lemmas connecting the addition, subtraction and negation additive group operations, but a far thinner collection of results for multiplication, division and inverse multiplicative group operations, despite the fact that the former can be generated easily from the latter via `to_additive`.

In  #9548 I require multiplicative forms of the existing `sub_add_cancel` and `neg_sub` lemmas. This PR refactors them as the equivalent multiplicative results and then recovers `sub_add_cancel` and `neg_sub` via `to_additive`. There is a complication in that unfortunately `group_with_zero` already has lemmas named `inv_div` and `div_mul_cancel`. I have worked around this by naming the lemmas in this PR `inv_div'` and `div_mul_cancel'` and then manually overriding the names generated by `to_additive`. Other suggestions as to how to approach this welcome.
@mans0954 mans0954 mentioned this pull request Nov 25, 2021
Closed
@mans0954 mans0954 mentioned this pull request Nov 27, 2021
Closed
1 task
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 3, 2021
@mans0954
Copy link
Collaborator Author

mans0954 commented Dec 4, 2021

I think everything of use in this PR has now been merged via other smaller PRs, so closing.

@mans0954 mans0954 closed this Dec 4, 2021
@mans0954 mans0954 mentioned this pull request Apr 9, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@semorrison semorrison semorrison left review comments

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes merge-conflict Please `git merge origin/master` then a bot will remove this label.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@mans0954 @ocfnash @eric-wieser @semorrison @jcommelin