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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(MeasureTheory/Constructions/Pi): add measurePreserving_pi #14185

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(MeasureTheory/Constructions/Pi): add measurePreserving_pi #14185

wants to merge 5 commits into from

Conversation

xroblot
Copy link
Collaborator

@xroblot xroblot commented Jun 27, 2024 •
edited
Loading

See the Zulip thread

Open in Gitpod

@xroblot xroblot added awaiting-review awaiting-CI t-measure-probability Measure theory / Probability theory labels Jun 27, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Jun 27, 2024 •
edited
Loading

PR summary 98d4aa137e

Import changes

No significant changes to the import graph

Declarations diff

+ measurePreserving_pi
+ volume_preserving_pi

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>

@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jun 27, 2024
@xroblot xroblot added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 28, 2024
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jun 28, 2024
@xroblot xroblot added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 28, 2024
@kim-em kim-em requested a review from sgouezel July 14, 2024 20:32
@urkud
Copy link
Member

urkud commented Jul 15, 2024

Thanks! 🎉
bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 15, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 15, 2024
@xroblot
feat(MeasureTheory/Constructions/Pi): add measurePreserving_pi (#14185
2611092 
)

See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/MeasureTheory.2EmeasurePreserving_pi/near/447399178)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 15, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(MeasureTheory/Constructions/Pi): add measurePreserving_pi [Merged by Bors] - feat(MeasureTheory/Constructions/Pi): add measurePreserving_pi Jul 15, 2024
@mathlib-bors mathlib-bors bot closed this Jul 15, 2024
@mathlib-bors mathlib-bors bot deleted the xfr_measurepreserving_pi branch July 15, 2024 00:22
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel Awaiting requested review from sgouezel

Assignees
No one assigned
Labels
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.
4 participants
@xroblot @urkud @sgouezel @kim-em