Commit 2019-05-24 05:29 c6a7f300
View on Github →refactor(set_theory/ordinal): shorten proof of well_ordering_thm (#1078)
- refactor(set_theory/ordinal): shorten proof of well_ordering_thm§
- Update ordinal.lean
- Update ordinal.lean
- Update ordinal.lean
- Improve readability
- shorten proof
- Shorten proof