mathlib3
2c1d8ca2 - chore(analysis/special_functions): Reduce imports in special_functions (#18909)

Commit
2 years ago
chore(analysis/special_functions): Reduce imports in special_functions (#18909) Remove a bunch of imports in `analysis/special_functions` and `analysis/calculus` which are unnecessary by transitivity, and a few more which are genuinely nontrivial (i.e. the import isn't in the transitive closure of the other imports) but nonetheless aren't needed for the file to compile.
Author
Parents
Loading