mathlib
37783539 - feat(set_theory/ordinal_arithmetic): `enum_ord univ = id` (#12391)

Commit

4 years ago

feat(set_theory/ordinal_arithmetic): `enum_ord univ = id` (#12391) Co-authored-by: Johan Commelin <johan@commelin.net>

Author

vihdzp

Parents