[Merged by Bors] - feat(Combinatorics/SimpleGraph): takeUntil properties by pimotte · Pull Request #21250 · leanprover-community/mathlib4

pimotte · 2025-01-30T08:47:19Z

Adds various results on takeUntil.
In preparation for a proof of Tutte's theorem.

depends on: [Merged by Bors] - chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk #21981

Zulip thread on Tutte's

github-actions · 2025-01-30T08:48:10Z

PR summary 3ec1b86f6e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ IsCycle.isPath_of_append_left
+ IsCycle.isPath_of_append_right
+ IsCycle.isPath_takeUntil
+ Nil.append
+ end_mem_tail_support
+ endpoint_not_mem_support_takeUntil
+ getVert_takeUntil
+ length_takeUntil_lt
+ mem_support_of_adj_toSubgraph
+ nil_append_iff
+ nil_takeUntil
+ not_mem_support_takeUntil_takeUntil
+ snd_takeUntil
+ takeUntil_cons
+ takeUntil_first
+ takeUntil_takeUntil

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

Co-authored-by: Yaël Dillies <[email protected]>

YaelDillies

Thanks!

maintainer delegate

github-actions · 2025-01-31T15:59:40Z

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

…b4 into PO_takeUntil

pimotte · 2025-02-17T09:34:41Z

@YaelDillies Backmerging master put Walk.lean over the line limit, so I took the liberty of splitting off the section on takeUntil, dropUntil and rotate into WalkDecomp.lean. I'm happy to revert this if we don't want to do it in this PR, but splitting it was fairly painless. I think it does make sense to do it now, since it was also the section I was heavily editing.

For the ease of maintainer review: diff to master before the split, diff of the refactoring

YaelDillies

Indeed it would be better if you could make the move in a quick preliminary PR

pimotte · 2025-02-17T10:36:52Z

Indeed it would be better if you could make the move in a quick preliminary PR

Done: #21981

Since Walk is becoming a long file, and with #21250 would be pushed over the limit, this PR extracts the WalkDecomp section, along with one lemma that depends on it to a seperate file. Co-authored-by: Pim Otte <[email protected]>

mathlib4-dependent-issues-bot · 2025-02-21T12:44:17Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk #21981~~
By Dependent Issues (🤖). Happy coding!

YaelDillies

Thanks! 🚀

maintainer merge

github-actions · 2025-02-21T13:55:51Z

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

ocfnash

Thanks. One minor suggestion but otherwise LGTM

bors d+

mathlib-bors · 2025-02-21T17:19:54Z

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

Co-authored-by: Oliver Nash <[email protected]>

pimotte · 2025-02-24T06:45:06Z

bors r+

Adds various results on takeUntil. In preparation for a proof of Tutte's theorem. Co-authored-by: Pim Otte <[email protected]>

mathlib-bors · 2025-02-24T06:56:13Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: feat(Polynomial): polynomial sequences are bases for R[X] (#20846) feat: monoidal structure on Hopf algebras (#12011) feat(DiscreteValuationRing): addVal_eq_zero_iff (#21154) refactor(Cache): refactor getPackageDir to not use manually provided package directories (#21817) feat(CategoryTheory): categories of homological complexes have a separator (#20229) chore(Data/Complex): deprecate `Complex.abs` (#21995) feat: uncountable instances for `Ordinal` and isomorphic types (#18547) feat(Data/Set/Card): a few missing lemmas (#22186) feat: discrete topological spaces are 0-manifolds (#22105) feat(Data/Matroid/Loop): matroid loops (#22045) feat(SetTheory/Ordinal/Nimber/Field): Nimber division (#19066) feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162) feat(Data/Matroid/Circuit): matroid cocircuits (#21692) feat(Topology/Compactification/OnePoint): generalize instance (#22179) feat(Combinatorics/SimpleGraph): takeUntil properties (#21250) feat(Tactic): `pnat_to_nat` and `enat_to_nat` tactics (#21602) refactor: move `Polynomial.coeffs` and related results (#22225) chore: add AlgHom.ker_coe_equiv, resolve porting notes and erws (#22019) refactor(Order/Category): `ConcreteCategory` instance for `\omegaCPO` (#21478) feat(CategoryTheory): Grothendieck categories have a coseparator (#22224) feat: tweak calc widget (#22170) feat(CategoryTheory): the Freyd-Mitchell embedding theorem (#22222) chore(CategoryTheory): turn more `simp` into `simps!` (#22223) feat(CategoryTheory): the category of ind-objects is Grothendieck abelian (#21606) feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in `SimplexCategoryGenRel` (#21743) chore(CategoryTheory/DiscreteCategory): turn `simp` to `simps!` (#22217) feat(Analysis/Asymptotics): exponential growth of a sequence (#21178) feat(CategoryTheory): sigmaConst preserves monomorphisms (#21599) feat(RingTheory/Cotangent): `liftBaseChange` is injective for localizations (#21037) chore(CategoryTheory): fix incorrect name (#22210) feat(CategoryTheory): `IsPullback` version of 'pullback of iso is iso' (#22211) feat(CategoryTheory): pullbacks in functor categories (#22209) feat(CategoryTheory): detecting limit cones over connected diagrams (#22192) feat(LinearAlgebra): add theorems for injective/surjective/bijective compositions of bilinear maps (#21491)

Adds various results on takeUntil. In preparation for a proof of Tutte's theorem. Co-authored-by: Pim Otte <[email protected]>

pimotte added 6 commits January 29, 2025 15:58

feat(Combinatorics/SimpleGraph): takeUntil development

096757e

Pre-review

019d688

Golfing

e26efe0

Cleanup

d40f639

Renaming

ec0734a

Naming

68d081a

pimotte added the t-combinatorics Combinatorics label Jan 30, 2025

pimotte assigned YaelDillies Jan 30, 2025

pimotte unassigned YaelDillies Jan 30, 2025

pimotte requested a review from YaelDillies January 30, 2025 08:52

YaelDillies reviewed Jan 30, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2025

pimotte and others added 4 commits January 30, 2025 10:11

Apply suggestions from code review

f972307

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

1007949

Co-authored-by: Yaël Dillies <[email protected]>

post-review cleanup

71a7ed8

Split result into more general components

fcd3637

pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025

pimotte added 2 commits January 31, 2025 11:40

Tiny cleanup

ee2caad

Golfing

444f773

YaelDillies reviewed Jan 31, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025

pimotte and others added 4 commits January 31, 2025 14:49

Apply suggestions from code review

3aba53c

Co-authored-by: Yaël Dillies <[email protected]>

Post PR fixes

4389ddd

Name

c645b7e

Nil.append

91fdd12

pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025

YaelDillies approved these changes Jan 31, 2025

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Walk.lean Outdated

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 31, 2025

pimotte added 3 commits February 17, 2025 09:48

Line fix

b572c39

Merge branch 'PO_takeUntil' of github.com:leanprover-community/mathli…

f0ab190

…b4 into PO_takeUntil

Some golfs

135a8a4

YaelDillies reviewed Feb 17, 2025

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/Path.lean Outdated

pimotte mentioned this pull request Feb 17, 2025

[Merged by Bors] - chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk #21981

Closed

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 Feb 17, 2025

pimotte added 2 commits February 21, 2025 10:19

Extra lemma

c404256

Implicit variables

219e629

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 Feb 21, 2025

pimotte added 2 commits February 21, 2025 14:08

Merge remote-tracking branch 'origin/master' into PO_takeUntil

74c2e63

Review comments

1c941c9

YaelDillies approved these changes Feb 21, 2025

View reviewed changes

ocfnash approved these changes Feb 21, 2025

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean Outdated

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 21, 2025

Update Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean

3ec1b86

Co-authored-by: Oliver Nash <[email protected]>

mathlib-bors bot pushed a commit that referenced this pull request Feb 24, 2025

feat(Combinatorics/SimpleGraph): takeUntil properties (#21250)

8c8ef3c

Adds various results on takeUntil. In preparation for a proof of Tutte's theorem. Co-authored-by: Pim Otte <[email protected]>

mathlib-bors bot changed the title ~~feat(Combinatorics/SimpleGraph): takeUntil properties~~ [Merged by Bors] - feat(Combinatorics/SimpleGraph): takeUntil properties Feb 24, 2025

mathlib-bors bot closed this Feb 24, 2025

mathlib-bors bot deleted the PO_takeUntil branch February 24, 2025 06:56

Champitoad pushed a commit that referenced this pull request Feb 25, 2025

feat(Combinatorics/SimpleGraph): takeUntil properties (#21250)

c59583e

Adds various results on takeUntil. In preparation for a proof of Tutte's theorem. Co-authored-by: Pim Otte <[email protected]>

Conversation

pimotte commented Jan 30, 2025 • edited by ocfnash Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3ec1b86f6e

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Jan 31, 2025

Uh oh!

pimotte commented Feb 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

pimotte commented Feb 17, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Feb 21, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Feb 21, 2025

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 21, 2025

Uh oh!

pimotte commented Feb 24, 2025

Uh oh!

mathlib-bors bot commented Feb 24, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

pimotte commented Jan 30, 2025 •

edited by ocfnash

Loading

github-actions bot commented Jan 30, 2025 •

edited

Loading

pimotte commented Feb 17, 2025 •

edited

Loading