mathlib
fae00c7c - chore(analysis/special_functions): move measurability statements to measure_theory folder (#8006)

Commit
4 years ago
chore(analysis/special_functions): move measurability statements to measure_theory folder (#8006) Make sure that measure theory is not imported in basic files defining trigonometric functions and real powers. The measurability of these functions is postponed to a new file `measure_theory.special_functions`.
Author
Parents
Loading