Commit 2022-05-17 15:35 da201ad4

View on Github →

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.

Estimated changes

Modified src/set_theory/game/nim.lean

Modified src/set_theory/ordinal/arithmetic.lean

deleted def ordinal.opow

added theorem ordinal.opow_def

deleted def ordinal.sub

Modified src/set_theory/ordinal/basic.lean

deleted theorem ordinal.le_total

deleted def ordinal.lt

Modified src/set_theory/ordinal/notation.lean

modified theorem nonote.repr_opow