Skip to content

[Merged by Bors] - feat(Order/Antisymmetrization): AntisymmRel lemmas#19571

Closed
vihdzp wants to merge 25 commits intomasterfrom
vi.antisymm
Closed

[Merged by Bors] - feat(Order/Antisymmetrization): AntisymmRel lemmas#19571
vihdzp wants to merge 25 commits intomasterfrom
vi.antisymm

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Nov 28, 2024

These are mostly ported from SetTheory.PGame.Equiv.


Open in Gitpod

@vihdzp vihdzp added the t-order Order theory label Nov 28, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 28, 2024

messageFile.md

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 28, 2024
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Nov 28, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 11, 2024
@vihdzp vihdzp requested a review from YaelDillies December 11, 2024 10:54
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 13, 2025
vihdzp and others added 3 commits January 13, 2025 07:17
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@github-actions
Copy link
Copy Markdown

messageFile.md

@vihdzp vihdzp mentioned this pull request Jan 20, 2025
10 tasks
@github-actions
Copy link
Copy Markdown

messageFile.md

@vihdzp vihdzp removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 20, 2025
@github-actions
Copy link
Copy Markdown

PR summary e0b625b78b

Import changes exceeding 2%

% File
+2.50% Mathlib.Order.Antisymmetrization

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Order.Antisymmetrization 200 205 +5 (+2.50%)
Import changes for all files
Files Import difference
Mathlib.Order.Antisymmetrization 5

Declarations diff

+ AntisymmRel.antisymmRel_congr
+ AntisymmRel.antisymmRel_congr_left
+ AntisymmRel.antisymmRel_congr_right
+ AntisymmRel.ge
+ AntisymmRel.le
+ AntisymmRel.le_congr
+ AntisymmRel.le_congr_left
+ AntisymmRel.le_congr_right
+ AntisymmRel.lt_congr
+ AntisymmRel.lt_congr_left
+ AntisymmRel.lt_congr_right
+ AntisymmRel.rfl
+ AntisymmRel.trans_le
+ AntisymmRel.trans_lt
+ LE.le.lt_or_antisymmRel
+ LE.le.trans_antisymmRel
+ LT.lt.trans_antisymmRel
+ _
+ antisymmRel_comm
+ instance : @Trans α α α (AntisymmRel (· ≤ ·)) (· < ·) (· < ·)
+ instance : @Trans α α α (AntisymmRel (· ≤ ·)) (· ≤ ·) (· ≤ ·)
+ instance : @Trans α α α (· < ·) (AntisymmRel (· ≤ ·)) (· < ·)
+ instance : @Trans α α α (· ≤ ·) (AntisymmRel (· ≤ ·)) (· ≤ ·)
+ instance : IsSymm α (AntisymmRel r)
+ instance [IsRefl α r] : IsRefl α (AntisymmRel r)
+ instance [IsTrans α r] : IsTrans α (AntisymmRel r)
+ le_iff_lt_or_antisymmRel
+ le_of_antisymmRel_of_le
+ le_of_le_of_antisymmRel
+ lt_of_antisymmRel_of_lt
+ lt_of_lt_of_antisymmRel
+ rel_congr
+ rel_congr_left
+ rel_congr_right

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.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks! 🚀

maintainer merge

@github-actions
Copy link
Copy Markdown

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 20, 2025
@vihdzp vihdzp requested review from tristan-f-r and removed request for tristan-f-r January 26, 2025 12:27
@eric-wieser
Copy link
Copy Markdown
Member

bors merge

Thanks!

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 26, 2025
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 26, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Order/Antisymmetrization): AntisymmRel lemmas [Merged by Bors] - feat(Order/Antisymmetrization): AntisymmRel lemmas Jan 26, 2025
@mathlib-bors mathlib-bors bot closed this Jan 26, 2025
@mathlib-bors mathlib-bors bot deleted the vi.antisymm branch January 26, 2025 14:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

large-import Automatically added label for PRs with a significant increase in transitive imports maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-order Order theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants