integrals): move lemmas out of namespace (#6778)

Commit

4 years ago

fix(analysis/special_functions/integrals): move lemmas out of namespace (#6778) Some lemmas should not have been moved into a namespace, so I fix that here.

Author

benjamindavidson

Parents

26fcfbc9

mathlib3 b0150a5d - fix(analysis/special_functions/integrals): move lemmas out of namespace (#6778)

mathlib3
b0150a5d - fix(analysis/special_functions/integrals): move lemmas out of namespace (#6778)