mathlib
9407b033 - chore(logic/equiv/basic): split into two files (#17038)

Commit
3 years ago
chore(logic/equiv/basic): split into two files (#17038) A fairly easy split of `logic.equiv.basic` into `logic.equiv.defs` (containing the stuff with very little prerequisites, and which suffices for many other files), and `logic.equiv.basic` (the stuff that requires other imports from around `logic.*`). `logic.equiv.basic` is still a ~1500 line file, so I'd like to split it further shortly. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading