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

[Merged by Bors] - feat: define AddConstEquiv #9726

Closed
wants to merge 35 commits into from
Closed

[Merged by Bors] - feat: define AddConstEquiv #9726

wants to merge 35 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Jan 13, 2024 •
edited
Loading

Also revert some scoped modifiers on simps.

Waiting for a benchmark.

Open in Gitpod

urkud added 5 commits January 13, 2024 14:43
@urkud
feat(Function/Conjugate): add Semiconj.inverse_left
8b5fa4e 
* Add `Function.semiconj_iff_comp_eq`
  and `Function.Semiconj.inverse_left`.
* Swap arguments of `Function.Semiconj.comp_left`.
  The old version is available as `Function.Semiconj.trans`.
* Add docstrings.
@urkud
Snapshot
ca7b1c8
@urkud
Snapshot
25e7056
@urkud
Merge branch 'YK-semiconj' into YK-add-const-equiv
98ed948
@urkud
feat: define AddConstEquiv
759f032
@urkud urkud added awaiting-review t-algebra Algebra (groups, rings, fields, etc) t-dynamics Dynamical Systems labels Jan 13, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jan 13, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jan 23, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 23, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 23, 2024
ericrbg
ericrbg reviewed Feb 5, 2024
View reviewed changes
@fpvandoorn fpvandoorn added the awaiting-author A reviewer has asked the author a question or requested changes label Apr 5, 2024
@eric-wieser
Copy link
Member

Should this be written in terms of VAdd instead? Then you could show that all affine equivalences are VAddConstEquivs

@urkud
Copy link
Member Author

urkud commented May 21, 2024

@eric-wieser The only application I have in mind is a lift of a circle map/homeomorphism to the real line. Do you have some applications of VAdd version in mind? I mean, some nontrivial result that will benefit from this generalization. If no, then I would prefer to postpone this generalization until we need it.

@urkud
Copy link
Member Author

urkud commented Jun 29, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit d345bdf.
There were no significant changes against commit 03cf112.

@urkud urkud requested a review from sgouezel July 4, 2024 13:32
YaelDillies
YaelDillies reviewed Jul 17, 2024
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 17, 2024
@urkud urkud added awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 17, 2024
YaelDillies
YaelDillies reviewed Jul 18, 2024
View reviewed changes
@YaelDillies
Copy link
Collaborator

Let's see whether it now works from my phone

maintainer merge

@github-actions GitHub Actions
Copy link

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

@kim-em
Copy link
Contributor

kim-em commented Jul 19, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jul 19, 2024
@urkud
feat: define AddConstEquiv (#9726)
966e2d6 
Also revert some `scoped` modifiers on `simp`s.
@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 19, 2024
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: define AddConstEquiv [Merged by Bors] - feat: define AddConstEquiv Jul 19, 2024
@mathlib-bors mathlib-bors bot closed this Jul 19, 2024
@mathlib-bors mathlib-bors bot deleted the YK-add-const-equiv branch July 19, 2024 00:35
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

@ericrbg ericrbg ericrbg left review comments

@sgouezel sgouezel Awaiting requested review from sgouezel

Assignees
No one assigned
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-dynamics Dynamical Systems
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
8 participants
@urkud @leanprover-community-mathlib4-bot @eric-wieser @leanprover-bot @YaelDillies @kim-em @ericrbg @fpvandoorn