Skip to content

[Merged by Bors] - chore(Analysis/InnerProductSpace): LinearMap.isAdjointPair_inner generalization to isROrC#8309

Closed
mcdoll wants to merge 1 commit intomasterfrom
mcdoll/adjoint_pair2
Closed

[Merged by Bors] - chore(Analysis/InnerProductSpace): LinearMap.isAdjointPair_inner generalization to isROrC#8309
mcdoll wants to merge 1 commit intomasterfrom
mcdoll/adjoint_pair2

Conversation

@mcdoll
Copy link
Copy Markdown
Member

@mcdoll mcdoll commented Nov 10, 2023

I forgot in the previous PR (#8295) that there are two versions of the adjoint.


Sorry for that.

Open in Gitpod

@mcdoll mcdoll added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-analysis Analysis (normed *, calculus) labels Nov 10, 2023
@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 Nov 10, 2023
@eric-wieser
Copy link
Copy Markdown
Member

bors merge

Thanks!

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 10, 2023
mathlib-bors bot pushed a commit that referenced this pull request Nov 10, 2023
…ralization to isROrC (#8309)

I forgot in the previous PR (#8295) that there are two versions of the adjoint.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 10, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Analysis/InnerProductSpace): LinearMap.isAdjointPair_inner generalization to isROrC [Merged by Bors] - chore(Analysis/InnerProductSpace): LinearMap.isAdjointPair_inner generalization to isROrC Nov 10, 2023
@mathlib-bors mathlib-bors bot closed this Nov 10, 2023
@mathlib-bors mathlib-bors bot deleted the mcdoll/adjoint_pair2 branch November 10, 2023 12:36
grunweg pushed a commit that referenced this pull request Dec 15, 2023
…ralization to isROrC (#8309)

I forgot in the previous PR (#8295) that there are two versions of the adjoint.
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-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants