mathlib

da201ad4 - chore(set_theory/ordinal/{basic, arithmetic}): Inline instances (#14076)

chore(set_theory/ordinal/{basic, arithmetic}): Inline instances (#14076) We inline various definition in the `ordinal` instances, thus avoiding protected (or unprotected!) definitions that are only used once.