Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-25 07:24 ccf646d3

View on Github →

chore(set_theory/ordinal): use a protected lemma to drop a nolint (#2805)

Estimated changes

added theorem ordinal.div_def
deleted def ordinal.div_def