mathlib
d3006bad - chore(init_/): remove this directory (#3227)

Commit
5 years ago
chore(init_/): remove this directory (#3227) * remove `init_/algebra`; * move `init_/data/nat` to `data/nat/basic`; * move `init_/data/int` to `data/int/basic`.
Author
Parents
Loading