mathlib3
27c4241b - feat(set_theory/ordinal/arithmetic): `has_exists_add_of_le` instance for `ordinal` (#14499)

Commit
3 years ago
feat(set_theory/ordinal/arithmetic): `has_exists_add_of_le` instance for `ordinal` (#14499)
Author
Parents
Loading