mathlib
363e2441 - Revert "feat(*): minimise imports to those used"

Commit

4 years ago

Revert "feat(*): minimise imports to those used" This reverts commit 2bcfb2886c55e97e486edf86b0dd07fadf07ab62.

Author

alexjbest

Parents