mathlib3
refactor(set_theory/ordinal): shorten proof of well_ordering_thm
#1078

Merged

refactor(set_theory/ordinal): shorten proof of well_ordering_thm #1078

mergify merged 7 commits into master from well-ordering-thm

refactor(set_theory/ordinal): shorten proof of well_ordering_thm§

7d62a9f8

ChrisHughes24 requested a review 7 years ago

Update ordinal.lean

767ad0cb

Update ordinal.lean

4887b49b

Update ordinal.lean

084b4eae

Improve readability

c5458841

digama0 commented on 2019-05-24

shorten proof

9645b0b3

Shorten proof

ccf5dea2

digama0 approved these changes on 2019-05-24

digama0 added ready-to-merge

mergify merged c6a7f300 into master 7 years ago

mergify deleted the well-ordering-thm branch 7 years ago

Reviewers

digama0

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone