Skip to content

Commit

Permalink
chore(measure_theory/function/special_functions): import inner_produc…
Browse files Browse the repository at this point in the history
…t_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.
  • Loading branch information
RemyDegenne committed Nov 4, 2021
1 parent b890836 commit 2129d05
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/measure_theory/function/special_functions.lean
Expand Up @@ -6,7 +6,7 @@ Authors: Yury Kudryashov

import analysis.special_functions.pow
import analysis.special_functions.trigonometric.arctan
import analysis.inner_product_space.calculus
import analysis.inner_product_space.basic
import measure_theory.constructions.borel_space

/-!
Expand Down

0 comments on commit 2129d05

Please sign in to comment.