Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-23 05:21 5931c5cb

View on Github →

lint(set_theory/ordinal): fix def/lemma (#6369)

Estimated changes

added theorem cardinal.ord_eq_min
deleted def cardinal.ord_eq_min