Euler Characteristic

Stream: Is there code for X?

[Rida Hamadani]

Do we have Euler's characteristic in Mathlib? More specifically, do we have Euler's polyhedron formula? I saw that @Yaël Dillies defined the characteristic here, was this ported?

[Yaël Dillies]

We don't even have planar graphs! @Kalle Kytölä and I are seriously thinking about formalising them, though

[Yaël Dillies]

Rida Hamadani said:

@Yaël Dillies defined the characteristic here, was this ported?

It was mostly ported in LeanCamCombi, but note that there is still stuff under the #exit. I welcome PRs to push the #exit further down!

[Rida Hamadani]

I see, thank you!