Mathlib v3 is deprecated. Go to Mathlib v4

Def ordinal.div_def

Modification history

2020-05-25 07:24
src/set_theory/ordinal.lean
chore(set_theory/ordinal): use a `protected lemma` to drop a `nolint` (#2805)
Deleted ordinal.div_defView on Github →
2020-02-24 15:43
src/set_theory/ordinal.lean
feat(tactic/lint): support @[nolint unused_arguments] (#2041) …
Modified ordinal.div_defView on Github →
2019-10-24 06:28
src/set_theory/ordinal.lean
chore(*): pass dup_namespace and def_lemma lint tests (#1599) …
Modified ordinal.div_defView on Github →
2019-09-22 04:34
src/set_theory/ordinal.lean
chore(*): fix various issues reported by `sanity_check_mathlib` (#1469) …
Modified ordinal.div_defView on Github →
2017-12-23 10:06
data/ordinal.lean
feat(data/ordinal): mul, div, mod, dvd, sub, power
Added ordinal.div_defView on Github →