SimpleGraph: bipartite iff all cycles have even length

Stream: mathlib4

[Yue Sun]

Hi, I submitted a PR proving the classical characterization of bipartite graphs:

A simple graph is bipartite if and only if all of its cycles have even length.

I am aware of Nick Adfor's contributions, and as a co-author, I made some changes to the original code.

Details can be found at the link below.

PR: https://github.com/leanprover-community/mathlib4/pull/33431

The proof is for SimpleGraph and is based on the existing notion of cycles.

CI is currently green.

I would appreciate feedback in particular on:

• whether the statement and naming are idiomatic,
• and whether the proof structure fits mathlib style.

Thanks!

[Nick Adfor]

cc @Snir Broshi

[Nick Adfor]

Snir Broshi said:

Nick Adfor said:

I'm tired of discussing distribution but I just want to make sure that everyone here are able to find the authors' Zulip and GitHub account and email

Can you ping Sun Yue here then?

It is here now.