mathlib
d990681c - docs(set_theory/ordinal): Remove mention of `omin` from docs (#12224)

Commit

3 years ago

docs(set_theory/ordinal): Remove mention of `omin` from docs (#12224) #11867 replaced `omin` by `Inf`. We remove all mentions of it from the docs.

Author

vihdzp

Parents