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: namespace some IsSelfAdjoint lemmas #14211

Closed
wants to merge 4 commits into from

Conversation

j-loreaux
Copy link
Collaborator

Per this Zulip discussion we choose to namespace (and protect) a few lemmas about IsSelfAdjoint.


Open in Gitpod

@j-loreaux j-loreaux added awaiting-review awaiting-CI t-algebra Algebra (groups, rings, fields, etc) labels Jun 27, 2024
Copy link

PR summary ac50c1f301

Import changes

No significant changes to the import graph


Declarations diff

+ add_star_self
+ intCast
+ natCast
+ nnratCast
+ ofNat
+ one
+ ratCast
+ star_add_self
+ zero
- _root_.isSelfAdjoint_add_star_self
- _root_.isSelfAdjoint_intCast
- _root_.isSelfAdjoint_natCast
- _root_.isSelfAdjoint_nnratCast
- _root_.isSelfAdjoint_ofNat
- _root_.isSelfAdjoint_one
- _root_.isSelfAdjoint_ratCast
- _root_.isSelfAdjoint_star_add_self
- _root_.isSelfAdjoint_zero

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

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

@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 Jun 28, 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 Jun 28, 2024
@kim-em
Copy link
Contributor

kim-em commented Jul 1, 2024

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 1, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 1, 2024
Per this [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20convention/near/447491526) we choose to namespace (and protect) a few lemmas about `IsSelfAdjoint`.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 1, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Jul 1, 2024
Per this [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20convention/near/447491526) we choose to namespace (and protect) a few lemmas about `IsSelfAdjoint`.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: namespace some IsSelfAdjoint lemmas [Merged by Bors] - chore: namespace some IsSelfAdjoint lemmas Jul 1, 2024
@mathlib-bors mathlib-bors bot closed this Jul 1, 2024
@mathlib-bors mathlib-bors bot deleted the j-loreaux/namespace-IsSelfAdjoint-lemmas branch July 1, 2024 14:30
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
Per this [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20convention/near/447491526) we choose to namespace (and protect) a few lemmas about `IsSelfAdjoint`.
@adomani adomani mentioned this pull request Aug 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
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