mathlib
2129d053 - chore(measure_theory/function/special_functions): import inner_product_space.basic instead of inner_product_space.calculus (#10159)

Commit
4 years ago
chore(measure_theory/function/special_functions): import inner_product_space.basic instead of inner_product_space.calculus (#10159) Right now this changes almost nothing because other imports like `analysis.special_functions.pow` depend on calculus, but I am changing that in other PRs. `measure_theory/function/special_functions` will soon not depend on calculus at all.
Author
Parents
Loading