mathlib
b9beca0b - chore(set_theory/ordinal): split into multiple files (#3517)

Commit
5 years ago
chore(set_theory/ordinal): split into multiple files (#3517) Split the file `ordinal.lean` into three files, and add docstrings for all definitions and file-level docstrings. This is just shuffling things around: no new content, no erased content. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Author
Parents
Loading