[SnirBroshi]

Define SimpleGraph.IsEulerian to be ∃ (v : V) (p : G.Walk v v), p.IsEulerian, and prove basic results.

Also show that in a connected Eulerian graph there exists an Eulerian circuit from any vertex.
This lets us take a circuit at a specific vertex, much like IsHamiltonian.exists_isHamiltonianCycle in Hamiltonian graphs.

---

[github-actions]

PR summary 42ccd789c9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ IsEulerian
+ IsEulerian.bot
+ IsEulerian.connected_of_forall_not_isIsolated
+ IsEulerian.even_degree
+ IsEulerian.exists_isEulerian_of_not_isIsolated
+ IsEulerian.exists_isEulerian_of_preconnected
+ IsEulerian.isCircuit_iff
+ IsEulerian.mem_support_of_preconnected
+ IsEulerian.nonempty
+ IsEulerian.of_bot
+ IsEulerian.rotate
+ isEulerian_and_ne_bot_iff
+ isEulerian_rotate

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 42ccd78).

• +20 new declarations
• −0 removed declarations

+SimpleGraph.IsEulerian
+SimpleGraph.IsEulerian.bot
+SimpleGraph.IsEulerian.casesOn
+SimpleGraph.IsEulerian.congr_simp
+SimpleGraph.IsEulerian.connected_of_forall_not_isIsolated
+SimpleGraph.IsEulerian.even_degree
+SimpleGraph.IsEulerian.exists_isEulerian
+SimpleGraph.IsEulerian.exists_isEulerian_of_not_isIsolated
+SimpleGraph.IsEulerian.exists_isEulerian_of_preconnected
+SimpleGraph.IsEulerian.mk
+SimpleGraph.IsEulerian.nonempty
+SimpleGraph.IsEulerian.rec
+SimpleGraph.IsEulerian.recOn
+SimpleGraph.Walk.IsEulerian.isCircuit_iff
+SimpleGraph.Walk.IsEulerian.mem_support_of_preconnected
+SimpleGraph.Walk.IsEulerian.of_bot
+SimpleGraph.Walk.IsEulerian.rotate
+SimpleGraph.Walk.isEulerian_rotate
+SimpleGraph.isEulerian_and_ne_bot_iff
+SimpleGraph.isEulerian_iff

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 42ccd789c9
Reference commit f32f0e99f9

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[YaelDillies]

Can you show that it is equivalent to \forall v, \exists p, ... under appropriate conditions?

[SnirBroshi]

Do you mean #41524 (comment)? As in iff versions of exists_isEulerian_of_not_isIsolated and exists_isEulerian_of_preconnected?
Even though it was kinda the first version of this PR (ab128a4, although the forall is in a different place) I kinda agree with Vlad that the reverse implication is trivial, so the iff is redundant.

[YaelDillies]

Sure, the reverse implication is trivial, but iffs let you rewrite, while implications don't (not exactly true now that we have grw, but you get the point)