Skip to content

[Merged by Bors] - move(RCLike): Move out of Data#11753

Closed
YaelDillies wants to merge 1 commit intomasterfrom
move_rclike
Closed

[Merged by Bors] - move(RCLike): Move out of Data#11753
YaelDillies wants to merge 1 commit intomasterfrom
move_rclike

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

RCLike is an analytic typeclass, hence should be under Analysis


Open in Gitpod

`RCLike` is an analytic typeclass, hence should be under `Analysis`
@fpvandoorn
Copy link
Copy Markdown
Member

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 29, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 29, 2024
`RCLike` is an analytic typeclass, hence should be under `Analysis`
@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 move(RCLike): Move out of Data [Merged by Bors] - move(RCLike): Move out of Data Mar 29, 2024
@mathlib-bors mathlib-bors bot closed this Mar 29, 2024
@mathlib-bors mathlib-bors bot deleted the move_rclike branch March 29, 2024 10:05
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
`RCLike` is an analytic typeclass, hence should be under `Analysis`
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
`RCLike` is an analytic typeclass, hence should be under `Analysis`
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
`RCLike` is an analytic typeclass, hence should be under `Analysis`
callesonne pushed a commit that referenced this pull request Apr 22, 2024
`RCLike` is an analytic typeclass, hence should be under `Analysis`
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