Commit 2023-07-18 05:18 a3e15d84
View on Github →chore: forward port #14324 (#5973) This is the remainder of the forward port of https://github.com/leanprover-community/mathlib/pull/14324. See https://leanprover-community.github.io/mathlib-port-status/file/set_theory/ordinal/natural_ops for the relevant #outofsync page.