Skip to content

[Merged by Bors] - chore: rename invOf lemmas to match inv lemmas#16590

Closed
eric-wieser wants to merge 6 commits intomasterfrom
eric-wieser/rename-invOf
Closed

[Merged by Bors] - chore: rename invOf lemmas to match inv lemmas#16590
eric-wieser wants to merge 6 commits intomasterfrom
eric-wieser/rename-invOf

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Sep 7, 2024 •
edited
Loading

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

@eric-wieser eric-wieser added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 7, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 7, 2024 •
edited
Loading

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
@eric-wieser eric-wieser mentioned this pull request Sep 7, 2024
Closed
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 7, 2024
YaelDillies
YaelDillies reviewed Sep 8, 2024
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 8, 2024
@eric-wieser @YaelDillies
Update Mathlib/Algebra/Group/Invertible/Defs.lean
e2faa85 
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
YaelDillies
YaelDillies approved these changes Sep 8, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@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

@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 8, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 8, 2024
@kbuzzard
Copy link
Copy Markdown
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
@eric-wieser
chore: rename invOf lemmas to match inv lemmas (#16590)
48b2de3 
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
Copy Markdown
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
@eric-wieser @bjoernkjoshanssen
chore: rename invOf lemmas to match inv lemmas (#16590)
2b68469 
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
@eric-wieser @bjoernkjoshanssen
chore: rename invOf lemmas to match inv lemmas (#16590)
f0fc311 
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
@eric-wieser @bjoernkjoshanssen
chore: rename invOf lemmas to match inv lemmas (#16590)
7e48ecc 
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
@4hma4d @eric-wieser
feat(LinearAlgebra/Matrix): Woodbury Identity (#16325)
facf1f9 
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>
@eric-wieser eric-wieser mentioned this pull request Sep 28, 2024
Closed
mathlib-bors bot pushed a commit that referenced this pull request Sep 29, 2024
@eric-wieser
fix(Matrix/Invertible): deprecated aliases should remain protected (#…
88304ce 
…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
@4hma4d @eric-wieser @fbarroero
feat(LinearAlgebra/Matrix): Woodbury Identity (#16325)
1965992 
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
@eric-wieser @fbarroero
fix(Matrix/Invertible): deprecated aliases should remain protected (#…
ea702c3 
…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

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@eric-wieser @kbuzzard @YaelDillies