{basic, arithmetic}): Remove redundant `function` namespace (#14133)

Commit

3 years ago

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

Author

vihdzp

Parents