[Merged by Bors] - feat: port Order.Zorn

[ADedecker]

No description provided.

[dupuisf]

Thanks!

bors d+

[bors]

✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[hrmacbeth]

bors r+

[bors]

Build failed:

• Build

[hrmacbeth]

It failed to build, apparently complaining about the local notation already being used in another file:

./././Mathlib.lean:1:0: error: import Mathlib.Order.Zorn failed, environment already contains
'«term_≺__3»._closed_6._cstage2' from Mathlib.Algebra.Order.EuclideanAbsoluteValue

Strange because this file successfully built before. I don't know if the problem was in deleting the comment

-- mathport name: «expr ≺ »

or in merging master. I'll try merging master first.

[ADedecker]

I've encountered this before, this is a bug (see here). The temporary fix is to give a name to the notation. I'm not at my computer right now, but you can have a look at what I did in Order.Antichain and Order.Chain to see the syntax for naming notations.

[hrmacbeth]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

And happy new year! 🎉

• Build
• Lint style