Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-20 09:08 b0150a5d

View on Github →

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.

Estimated changes

added theorem integral_cos
added theorem integral_exp
added theorem integral_id
added theorem integral_inv
added theorem integral_inv_of_neg
added theorem integral_inv_of_pos
added theorem integral_one
added theorem integral_one_div
added theorem integral_pow
added theorem integral_sin
added theorem integral_sin_pow_aux
added theorem integral_sin_pow_even
added theorem integral_sin_pow_odd
added theorem integral_sin_pow_pos