Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-01 17:57 fcfa2a40

View on Github →

refactor(set_theory/ordinal): restate well_ordering_thm (#1115) Define the relation rather than using an exists statement

Estimated changes

deleted theorem well_ordering_thm