Skip to content

[Merged by Bors] - feat: Not is involutive#11192

Closed
IvanRenison wants to merge 6 commits intomasterfrom
injective_not_IvanRenison
Closed

[Merged by Bors] - feat: Not is involutive#11192
IvanRenison wants to merge 6 commits intomasterfrom
injective_not_IvanRenison

Conversation

@IvanRenison
Copy link
Copy Markdown
Collaborator

@IvanRenison IvanRenison commented Mar 5, 2024

For using it in #9131

Open in Gitpod

@IvanRenison IvanRenison added easy < 20s of review time. See the lifecycle page for guidelines. t-logic Logic (model theory, etc) labels Mar 5, 2024
eric-wieser
eric-wieser reviewed Mar 5, 2024
View reviewed changes
@IvanRenison IvanRenison changed the title Add lemma injective_not Add lemma not_injective Mar 5, 2024
@IvanRenison IvanRenison added awaiting-review new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! and removed easy < 20s of review time. See the lifecycle page for guidelines. labels Mar 5, 2024
@IvanRenison IvanRenison requested a review from eric-wieser March 14, 2024 17:03
@urkud
Copy link
Copy Markdown
Member

urkud commented Mar 24, 2024 •
edited
Loading

Should it go to Logic/Lemmas or Logic/Function/Basic? I'm not sure.

BTW, could you please add not_bijective and not_surjective as well, all follow from not_involutive?

@IvanRenison
Copy link
Copy Markdown
Collaborator Author

IvanRenison commented Mar 25, 2024

Should it go to Logic/Lemmas or Logic/Function/Basic? I'm not sure.

I don't know, maybe yes. Any way, I don't know in witch part of Logic/Function/Basic should it be.
Tell me you what to do

@IvanRenison IvanRenison changed the title Add lemma not_injective Add lemma not_involutive and its trivial corollaries Mar 25, 2024
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Mar 29, 2024

It should go in Logic.Function.Basic. You can add it wherever you want but I think just before the definition of IsPartialInv is best.

@YaelDillies YaelDillies added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Mar 29, 2024
@YaelDillies YaelDillies mentioned this pull request Mar 29, 2024
Closed
2 tasks
@IvanRenison
Copy link
Copy Markdown
Collaborator Author

IvanRenison commented Mar 29, 2024

It should go in Logic.Function.Basic. You can add it wherever you want but I think just before the definition of IsPartialInv is best.

Before IsPartialInv it was not possible because Involutive is not defined yet. So I put it right after the namespace Involutive

@YaelDillies YaelDillies changed the title Add lemma not_involutive and its trivial corollaries feat: Not is involutive Mar 29, 2024
YaelDillies
YaelDillies reviewed Mar 29, 2024
View reviewed changes
YaelDillies
YaelDillies approved these changes Mar 29, 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!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 29, 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 Mar 29, 2024
@jcommelin jcommelin removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 29, 2024
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Mar 29, 2024

Thanks 🎉

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Mar 29, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 29, 2024
@IvanRenison
feat: Not is involutive (#11192)
160fb23
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 29, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Not is involutive [Merged by Bors] - feat: Not is involutive Mar 29, 2024
@mathlib-bors mathlib-bors bot closed this Mar 29, 2024
@mathlib-bors mathlib-bors bot deleted the injective_not_IvanRenison branch March 29, 2024 20:24
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@IvanRenison @xgenereux
feat: Not is involutive (#11192)
42b6711
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@IvanRenison @atarnoam
feat: Not is involutive (#11192)
22e717a
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@IvanRenison @uniwuni
feat: Not is involutive (#11192)
d3832ed
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@IvanRenison @callesonne
feat: Not is involutive (#11192)
276ee14
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

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-logic Logic (model theory, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@IvanRenison @urkud @YaelDillies @jcommelin @eric-wieser