feat: port Order.Ideal (#1985)

Co-authored-by: Johan Commelin <johan@commelin.net>

Author: int-y1

Mathlib.lean

@@ -791,6 +791,7 @@ import Mathlib.Order.Hom.Basic
 import Mathlib.Order.Hom.Bounded
 import Mathlib.Order.Hom.Order
 import Mathlib.Order.Hom.Set
+import Mathlib.Order.Ideal
 import Mathlib.Order.InitialSeg
 import Mathlib.Order.Iterate
 import Mathlib.Order.Lattice