free_pfpng.epi

Stream: condensed mathematics

[Kevin Buzzard]

Are there errors on master in src/free_pfpng/epi.lean and if so, did I cause them?

[Johan Commelin]

No, they come from a reason push by @Yaël Dillies. They needed a nonempty T assumption that is not yet satisfied at the place the lemma is used.

[Johan Commelin]

This should be fixed in a couple of hours. But I'm on a train atm.

[Johan Commelin]

So please ignore those errors for the time being.

[Yaël Dillies]

Unrelatingly, I forgot to open finset because all the files I work on already have it :sweat: