!3#17828 feat(combinatorics/quiver/covering)

Stream: PR reviews

[Scott Morrison]

This not-too-late mathlib3 PR by @Rémi Bottinelli had extensive review by @Yaël Dillies, but then the last message was a request from @Yaël Dillies for @Kyle Miller or @Bhavik Mehta to have a look.

Would one of the named people mind saying something about this PR, and what still needs to happen to get it over the line?

[Kyle Miller]

I did a bit of polishing work on this PR, and it's ready for another review (pinging @Yaël Dillies or @Bhavik Mehta ?).

There was a question by @Yaël Dillies of whether is_covering should be boosted to being equivalences rather than mere bijections, but let's leave that for a future investigation.

[Scott Morrison]

LGTM. I've hit merge. @Rémi Bottinelli, @Antoine Labelle, output from mathport should be ready in <24 hours, and hopefully then this file can be ported as for any other file. Please ping here if you'd like any help with the forward port!