mathlib3
91f053e1 - chore(*): simplify `data.real.cau_seq` import (#9197)

Commit
4 years ago
chore(*): simplify `data.real.cau_seq` import (#9197) Some files were still importing `data.real.cau_seq` when their dependency really was on `is_absolute_value`, which has been moved to `algebra.absolute_value`. Hopefully simplifying the dependency tree slightly reduces build complexity.
Author
Parents
Loading