feat: port SetTheory.Ordinal.Arithmetic (#2271)

Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com>
leanprover-community · Feb 16, 2023 · b9f402c · b9f402c
1 parent 1c14085
commit b9f402c
Show file tree

Hide file tree

Showing 2 changed files with 3,020 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -960,6 +960,7 @@ import Mathlib.SetTheory.Cardinal.Basic
 import Mathlib.SetTheory.Cardinal.Finite
 import Mathlib.SetTheory.Cardinal.SchroederBernstein
 import Mathlib.SetTheory.Lists
+import Mathlib.SetTheory.Ordinal.Arithmetic
 import Mathlib.SetTheory.Ordinal.Basic
 import Mathlib.Tactic.Abel
 import Mathlib.Tactic.Alias