Skip to content

[Merged by Bors] - chore(Group/Measure): drop a T2Space assumption#16284

Closed
urkud wants to merge 5 commits intomasterfrom
YK-drop-t2
Closed

[Merged by Bors] - chore(Group/Measure): drop a T2Space assumption#16284
urkud wants to merge 5 commits intomasterfrom
YK-drop-t2

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Aug 30, 2024

Open in Gitpod

@urkud urkud added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-measure-probability Measure theory / Probability theory labels Aug 30, 2024
@urkud urkud requested a review from sgouezel August 30, 2024 01:03
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 30, 2024 •
edited
Loading

PR summary dbba98c714

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Analysis.Fourier.RiemannLebesgueLemma 1795 1794 -1 (-0.06%)
Import changes for all files
Files Import difference
Mathlib.Analysis.Fourier.RiemannLebesgueLemma -1

Declarations diff

+ instance _root_.ContinuousLinearEquiv.isAddHaarMeasure_map
- MapContinuousLinearEquiv.isAddHaarMeasure
- _root_.ContinuousLinearEquiv.isAddHaarMeasure_map

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

@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 Aug 30, 2024
@urkud urkud removed the easy < 20s of review time. See the lifecycle page for guidelines. label Aug 30, 2024
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Aug 30, 2024

bors r+
Thanks!

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 30, 2024
grunweg
grunweg reviewed Aug 30, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

Nice, thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 30, 2024

🚀 Pull request has been placed on the maintainer queue by grunweg.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 30, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 30, 2024
@urkud
chore(Group/Measure): drop a T2Space assumption (#16284)
8eabcbe
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 30, 2024

Build failed (retrying...):

@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Aug 30, 2024

bors r-
Can you fix the lint, and then send it back to bors?
bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 30, 2024

✌️ 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.

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 30, 2024

Canceled.

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Aug 30, 2024
@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Aug 30, 2024

bors r-
bors delegate+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 30, 2024

✌️ 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.

@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Aug 30, 2024

Oh odd. I just got a new bors failure alert for a batch with this

urkud
urkud commented Aug 30, 2024
View reviewed changes
@urkud
Copy link
Copy Markdown
Member Author

urkud commented Aug 30, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Aug 30, 2024
@urkud
chore(Group/Measure): drop a T2Space assumption (#16284)
37b3e83
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Group/Measure): drop a T2Space assumption [Merged by Bors] - chore(Group/Measure): drop a T2Space assumption Aug 30, 2024
@mathlib-bors mathlib-bors bot closed this Aug 30, 2024
@mathlib-bors mathlib-bors bot deleted the YK-drop-t2 branch August 30, 2024 16:57
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@urkud @bjoernkjoshanssen
chore(Group/Measure): drop a T2Space assumption (#16284)
ad275c5
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@urkud @bjoernkjoshanssen
chore(Group/Measure): drop a T2Space assumption (#16284)
4e94ffb
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@urkud @bjoernkjoshanssen
chore(Group/Measure): drop a T2Space assumption (#16284)
e60fe88
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg grunweg left review comments

@sgouezel sgouezel Awaiting requested review from sgouezel

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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

@urkud @sgouezel @mattrobball @grunweg