feat: port SetTheory.Ordinal.Exponential (#2330)

leanprover-community · Feb 20, 2023 · be32c27 · be32c27
1 parent 189fab8
commit be32c27
Show file tree

Hide file tree

Showing 3 changed files with 486 additions and 459 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -984,6 +984,7 @@ import Mathlib.SetTheory.Cardinal.SchroederBernstein
 import Mathlib.SetTheory.Lists
 import Mathlib.SetTheory.Ordinal.Arithmetic
 import Mathlib.SetTheory.Ordinal.Basic
+import Mathlib.SetTheory.Ordinal.Exponential
 import Mathlib.SetTheory.Ordinal.NaturalOps
 import Mathlib.SetTheory.Ordinal.Topology
 import Mathlib.Tactic.Abel