Skip to content

Commit

Permalink
analysis: fix imports
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Oct 23, 2023
1 parent 64712be commit 982f1ef
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion src/exercises_sources/friday/analysis.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,11 @@ import analysis.normed_space.pi_Lp
import analysis.calculus.iterated_deriv
import analysis.calculus.mean_value
import analysis.calculus.implicit
import analysis.calculus.deriv.inv
import analysis.special_functions.exp_deriv
import measure_theory.integral.bochner
import measure_theory.measure.lebesgue
import measure_theory.measure.lebesgue.eq_haar
import measure_theory.integral.set_integral
import linear_algebra.matrix.trace


Expand Down

0 comments on commit 982f1ef

Please sign in to comment.