mathlib

4923cfc5 - chore(set_theory/ordinal): Removed redundant argument from `enum_typein` (#11049)