Mathlib v3 is deprecated. Go to Mathlib v4

Def cardinal.ord_eq_min

Modification history

2021-02-23 05:21
src/set_theory/ordinal.lean
lint(set_theory/ordinal): fix def/lemma (#6369)
Deleted cardinal.ord_eq_minView on Github →
2020-02-24 15:43
src/set_theory/ordinal.lean
feat(tactic/lint): support @[nolint unused_arguments] (#2041) …
Modified cardinal.ord_eq_minView on Github →
2019-10-24 06:28
src/set_theory/ordinal.lean
chore(*): pass dup_namespace and def_lemma lint tests (#1599) …
Modified cardinal.ord_eq_minView on Github →
2017-12-19 04:59
data/ordinal.lean
feat(data/ordinal): sup, cofinality, subtraction
Added cardinal.ord_eq_minView on Github →