Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-14 17:09 05997bda

View on Github →

chore(set_theory/ordinal/{basic, arithmetic}): Remove redundant function namespace (#14133)

Estimated changes

modified theorem not_injective_of_ordinal
modified theorem not_surjective_of_ordinal