Skip to content

[Merged by Bors] - feat: polar coords integral in a normed space#7693

Closed
urkud wants to merge 23 commits intomasterfrom
YK-meas-to-sphere
Closed

[Merged by Bors] - feat: polar coords integral in a normed space#7693
urkud wants to merge 23 commits intomasterfrom
YK-meas-to-sphere

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Oct 15, 2023 •
edited
Loading

@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes. t-measure-probability Measure theory / Probability theory labels Oct 15, 2023
github-actions[bot]
github-actions bot reviewed Oct 15, 2023
View reviewed changes
@urkud @github-actions
Update Mathlib/MeasureTheory/Measure/WithDensity.lean
1dd2574 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 15, 2023
@xroblot xroblot mentioned this pull request Oct 23, 2023
Closed
3 tasks
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 26, 2023
@xroblot xroblot mentioned this pull request Oct 30, 2023
Closed
6 tasks
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 30, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 1, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 1, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 1, 2023
@ghost
Copy link
Copy Markdown

ghost commented Nov 1, 2023

This PR/issue depends on:

@urkud urkud added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 2, 2023
sgouezel
sgouezel reviewed Nov 12, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, thanks!
bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 12, 2023

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Nov 12, 2023
@urkud
Copy link
Copy Markdown
Member Author

urkud commented Nov 13, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 13, 2023
mathlib-bors bot pushed a commit that referenced this pull request Nov 13, 2023
@urkud
feat: polar coords integral in a normed space (#7693)
69a0d13
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 13, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: polar coords integral in a normed space [Merged by Bors] - feat: polar coords integral in a normed space Nov 13, 2023
@mathlib-bors mathlib-bors bot closed this Nov 13, 2023
@mathlib-bors mathlib-bors bot deleted the YK-meas-to-sphere branch November 13, 2023 17:59
alexkeizer pushed a commit that referenced this pull request Nov 17, 2023
@urkud @alexkeizer
feat: polar coords integral in a normed space (#7693)
69a05e6
alexkeizer pushed a commit that referenced this pull request Nov 21, 2023
@urkud @alexkeizer
feat: polar coords integral in a normed space (#7693)
fc808f5
grunweg pushed a commit that referenced this pull request Dec 15, 2023
@urkud @grunweg
feat: polar coords integral in a normed space (#7693)
83d33a8
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

@github-actions github-actions[bot] github-actions[bot] left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@urkud @sgouezel