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] - chore: rename invOf lemmas to match inv lemmas #16590

Closed
wants to merge 6 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Sep 7, 2024

This follows on from #11530

In each case, I've added an example with the Group lemma, to make it easier to keep the names in sync.


Open in Gitpod

Copy link

github-actions bot commented Sep 7, 2024

PR summary e2faa85400

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ invOf_mul_cancel_left'
+ invOf_mul_cancel_right'
+ mul_invOf_cancel_left'
+ mul_invOf_cancel_right'
++ invOf_mul_cancel_left
++ invOf_mul_cancel_right
++ mul_invOf_cancel_left
++ mul_invOf_cancel_right
++-- invOf_mul_self_assoc
++-- mul_invOf_mul_self_cancel
++-- mul_invOf_self_assoc
++-- mul_mul_invOf_self_cancel

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@eric-wieser eric-wieser added the t-algebra Algebra (groups, rings, fields, etc) label Sep 7, 2024
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Sep 8, 2024
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@eric-wieser eric-wieser removed the awaiting-author A reviewer has asked the author a question or requested changes label Sep 8, 2024
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the followup!

maintainer merge

Copy link

github-actions bot commented Sep 8, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@kbuzzard
Copy link
Member

kbuzzard commented Sep 8, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Sep 8, 2024
This follows on from #11530

In each case, I've added an `example` with the `Group` lemma, to make it easier to keep the names in sync.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Sep 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: rename invOf lemmas to match inv lemmas [Merged by Bors] - chore: rename invOf lemmas to match inv lemmas Sep 8, 2024
@mathlib-bors mathlib-bors bot closed this Sep 8, 2024
@mathlib-bors mathlib-bors bot deleted the eric-wieser/rename-invOf branch September 8, 2024 12:13
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
This follows on from #11530

In each case, I've added an `example` with the `Group` lemma, to make it easier to keep the names in sync.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
This follows on from #11530

In each case, I've added an `example` with the `Group` lemma, to make it easier to keep the names in sync.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
This follows on from #11530

In each case, I've added an `example` with the `Group` lemma, to make it easier to keep the names in sync.
mathlib-bors bot pushed a commit that referenced this pull request Sep 26, 2024
This adds the [Woodbury Identity](https://en.wikipedia.org/wiki/Woodbury_matrix_identity).

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Woodbury.20identity/near/462245284)

Also corrects some bad deprecations introduced in #16590, which affected development of this PR.

Co-authored-by: Mohanad Ahmad



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
mathlib-bors bot pushed a commit that referenced this pull request Sep 29, 2024
…17242)

The originals were protected, and the deprecations break downstream code using the matching lemmas in the root namespace.

A second patch to #16590.
fbarroero pushed a commit that referenced this pull request Oct 2, 2024
This adds the [Woodbury Identity](https://en.wikipedia.org/wiki/Woodbury_matrix_identity).

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Woodbury.20identity/near/462245284)

Also corrects some bad deprecations introduced in #16590, which affected development of this PR.

Co-authored-by: Mohanad Ahmad



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
fbarroero pushed a commit that referenced this pull request Oct 2, 2024
…17242)

The originals were protected, and the deprecations break downstream code using the matching lemmas in the root namespace.

A second patch to #16590.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants