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] - chore: move List.Lex lemmas out of the List.Lex namespace #22935

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore: move List.Lex lemmas out of the List.Lex namespace #22935

wants to merge 3 commits into from
+17 −12

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Mar 14, 2025 •
edited by grunweg
Loading

This better matches the naming convention.

Open in Gitpod

@YaelDillies YaelDillies mentioned this pull request Mar 14, 2025
Open
@github-actions GitHub Actions
Copy link

github-actions bot commented Mar 14, 2025 •
edited
Loading

PR summary 82993a7cbf

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Lex.cons_iff
+ Lex.nil_left_or_eq_nil
+ Lex.singleton_iff
+ lex_cons_iff
+ lex_nil_or_eq_nil
+ lex_singleton_iff
- cons_iff
- nil_left_or_eq_nil
- singleton_iff

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).

@github-actions github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Mar 14, 2025
grunweg
grunweg reviewed Mar 16, 2025
View reviewed changes
Copy link
Collaborator

@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.

Thanks!
maintainer merge

@github-actions GitHub Actions
Copy link

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

@b-mehta
Copy link
Contributor

b-mehta commented Mar 16, 2025

Nice! (As an aside, the way you've split the commits here made this easy to review; thanks!)

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge labels Mar 16, 2025
mathlib-bors bot pushed a commit that referenced this pull request Mar 16, 2025
@YaelDillies
chore: move List.Lex lemmas out of the List.Lex namespace (#22935)
bce45b1 
This better matches the naming convention.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Mar 16, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: move List.Lex lemmas out of the List.Lex namespace [Merged by Bors] - chore: move List.Lex lemmas out of the List.Lex namespace Mar 16, 2025
@mathlib-bors mathlib-bors bot closed this Mar 16, 2025
@mathlib-bors mathlib-bors bot deleted the lex_cons_iff branch March 16, 2025 14:49
qawbecrdtey added a commit that referenced this pull request Mar 17, 2025
@qawbecrdtey @eric-wieser
@urkud @ScottCarnahan @plp127 @xroblot @sebzim4500 @JovanGerb @kebekus @vlad902 @YaelDillies
feat(Mathlib/Analysis/Normed/Lp/PiLp): Finished proof of `sumPiLpEqui…
986ada9 
…vProdLpPiLp` (#22993)

* feat: scalar tower instances for quotients (#22951)

We already have the `SMulCommClass` and `IsScalarTower` versions for `RingQuot`; this develops them for `Con` and `RingCon`, with the eventual aim of replacing `RingQuot` with `RingCon.Quotient`.

* chore(Order/Group/Abs): use `@[to_additive]` (#22468)

* feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic (#22843)

This PR adds some elementary results about the prime subfield of a characteristic p field, e.g., size is p, elements are integer multiples of one, and elements are characterized by being fixed by the p-th power map.

* docs(Data/Real/EReal): fix capitalization error (#22943)

Changes `Ereal` to `EReal` in the module docstring for `Data/Real/EReal`.

* chore(Ideal/Quotient): change `Fintype` to `Finite` (#22947)

As discussed [here](#22902 (comment))

* feat: add `norm_num` extensions for factorials (#8832)

Add `norm_num` extensions to evaluate `Nat.factorial`, `Nat.ascFactorial` and `Nat.descFactorial`.



Co-authored-by: Eric Wieser <[email protected]>

* perf(CategoryTheory/Limits/Shapes): reorder instance arguments (#22968)

This PR is in the same spirit as #22953.

The problem is that some instances about category theoretical limits have silly side conditions that end up searching through the whole algebraic type class hierarchy. This PR attempts to keep the type class search limited to category theoretical type classes.

* feat(LinearAlgebra/FreeModule/CardQuotient): compute indices of subgroups via determinant (#22940)

* feat: API for continuous extension of meromorphic functions (#22867)

Defines the normal form of meromorphic functions and provides API for continuous extension, as discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/API.20for.20continuous.20extension.20of.20meromorphic.20functions). More material will be provided in upcoming PRs.

This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

* feat(Data/Complex/Trigonometric): closer upper bound for cos 1 (#22945)

cos 1 is approximately 0.5403..., so this bound is fairly tight.

Co-authored-by: Vlad Tsyrklevich <[email protected]>

* chore: move `List.Lex` lemmas out of the `List.Lex` namespace (#22935)

This better matches the naming convention.

* working on it.

* Added sup_disjSum and inf_disjSum.

* Finished one branch.

* Finished proof.

---------

Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Yury G. Kudryashov <[email protected]>
Co-authored-by: Scott Carnahan <[email protected]>
Co-authored-by: plp127 <[email protected]>
Co-authored-by: Xavier Roblot <[email protected]>
Co-authored-by: Sebastian Zimmer <[email protected]>
Co-authored-by: JovanGerb <[email protected]>
Co-authored-by: Stefan Kebekus <[email protected]>
Co-authored-by: Vlad Tsyrklevich <[email protected]>
Co-authored-by: Vlad Tsyrklevich <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
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

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@YaelDillies @b-mehta @grunweg @leanprover-community-mathlib4-bot