mathlib3
b75113ac - chore(set_theory/game/ordinal): Remove redundant namespaces (#14039)

Commit

3 years ago

chore(set_theory/game/ordinal): Remove redundant namespaces (#14039)

Author

vihdzp

vihdzp

Parents

Loading