feat: port SetTheory.Ordinal.Notation (#2470)

Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Jon Eugster <eugster.jon@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Apurva Nakade <apurvnakade@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>
leanprover-community · Jun 21, 2023 · 7eebe3d · 7eebe3d
1 parent ca86563
commit 7eebe3d
Show file tree

Hide file tree

Showing 2 changed files with 1,381 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2660,6 +2660,7 @@ import Mathlib.SetTheory.Ordinal.CantorNormalForm
 import Mathlib.SetTheory.Ordinal.Exponential
 import Mathlib.SetTheory.Ordinal.FixedPoint
 import Mathlib.SetTheory.Ordinal.NaturalOps
+import Mathlib.SetTheory.Ordinal.Notation
 import Mathlib.SetTheory.Ordinal.Principal
 import Mathlib.SetTheory.Ordinal.Topology
 import Mathlib.SetTheory.ZFC.Basic