[Merged by Bors] - feat(Combinatorics/SimpleGraph): vertices in cycles#20602
[Merged by Bors] - feat(Combinatorics/SimpleGraph): vertices in cycles#20602
Conversation
|
messageFile.md |
YaelDillies
left a comment
There was a problem hiding this comment.
Ouch, +142 imports for importing Data.Set.Card. Maybe complain on Zulip that this is a huge price to pay to just write Set.ncard.
Do you think it would make your like any easier if we had a getCycleVert : ℤ → V function that's p.length-periodic? Then you wouldn't have to split cases on whether you are at the endpoint or not. Maybe @kmill has thoughts here too.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Strictly speaking I'm not just using
I think the results in this PR are more or less my way of abstracting the endpoint business, so from my perspective it doesn't help much beyond this. I can see how it would be nice here and give some cleaner results, so I'm not particularly leaning one way or the other. If we decide this is worthwhile I'd be happy to try to whip something up. |
YaelDillies
left a comment
There was a problem hiding this comment.
I think it's fine to leave both issues as is for now. Could you possibly just add a TODO for the ℤ-indexed sequence of vertices of a cycle?
maintainer delegate
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
✌️ pimotte can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
messageFile.md |
|
bors r+ |
This adds various lemmas on vertices in cycles: Non-equality, and the exact neighbors and size of the neighborSet, along with some smaller supporting lemmas for walks. In preparation for Tutte's theorem. Co-authored-by: Pim Otte <otte.pim@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
* polynomial-sequences: (149 commits) Aha, here's how to get Lean to stop showing S.elems' in the infoview. Try satisfying the linter gods again. Probably enough initial tidying to send the PR. Kill more temporary names. Touch more natDegree. Does protected satisfy the docstring linter? Bit shorter. More Quiet linters. Remove redundant imports. Copyright header and more twiddling. Rename lemma to 'degree_smul_of_leadingCoeff_rightRegular' and split out feat(Polynomial): polynomial sequences are bases for R[X] chore(Dynamics/PeriodicPts): don't import `MonoidWithZero` (#20765) chore(Associated): split out `Ring` results (#20737) feat(AlgebraicGeometry): flat morphisms of schemes (#19790) feat(AlgebraicGeometry): scheme-theoretic fibre (#19427) chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785) doc: typo (#20829) feat(CategoryTheory): condition for an induced functor between comma categories to be final (#20139) feat(1000.yaml): allow statements of theorems also (#20637) feat(Algebra/Homology/Embedding): homology of truncGE' (#19570) chore: cleanup many porting notes in Combinatorics (#20823) chore: eliminate porting notes about `deriving Fintype` (#20820) feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808) feat: define bases of root pairings (#20667) feat(Tactic): basic ConcreteCategory support for elementwise (#20811) feat(CategoryTheory): define unbundled `ConcreteCategory` class (#20810) chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809) feat: `CommSemiring (NonemptyInterval ℚ≥0)` (#20783) chore(yaml_check.py): re-format (#20807) feat: elementary estimate for Real.log (#20766) feat: definition of linear topologies (#14990) feat(RingTheory): flatness over a semiring (#19115) feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#19550) feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex (#19203) feat(Algebra/Ring): `RingEquiv.piUnique` (#20794) feat(RingTheory/LocalRing): add instance `Unique (MaximalSpectrum R)` for a local ring `R` (#20801) chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802) chore: restore `def` to `adicCompletion` (#20796) refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643) feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544) chore(Mathlib/Computability/TuringMachine): split file (#20790) feat(Data/Finset/Card): add `InjOn` and `SurjOn` versions of finset cardinality lemmas (#20753) feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752) feat(Set/Finite): a set is finite if its image and fibers are finite (#20751) chore: cleanup .gitignore files (#20795) feat(Topology/Group/Profinite): Profinite group is limit of finite group (#16992) feat(Combinatorics/SimpleGraph): vertices in cycles (#20602) CI: merge `bot_fix_style` actions (#20789) ...
This adds various lemmas on vertices in cycles: Non-equality, and the exact neighbors and size of the neighborSet, along with some smaller supporting lemmas for walks.
In preparation for Tutte's theorem.
Zulip thread on Tutte's
Context in my proof of Tutte's
These results are used in the proof to connect IsCycles to IsCycle.