Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-10 10:38 41f5c176

View on Github →

chore(set_theory/ordinal_arithmetic): Make auxiliary result private (#12562)

Estimated changes