Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-25 15:13 4e0c460a

View on Github →

chore(analysis/special_functions/integrals): reorganize file (#7351)

Estimated changes

Modified src/analysis/special_functions/integrals.lean

modified theorem integral_id

modified theorem integral_one

modified theorem integral_pow

modified theorem integral_sin_pow_aux

modified theorem integral_sin_pow_even

modified theorem integral_sin_pow_odd

modified theorem integral_sin_pow_pos

modified theorem integral_sin_pow_succ_succ

modified theorem interval_integral.interval_integrable.const_mul

modified theorem interval_integral.interval_integrable.div

modified theorem interval_integral.interval_integrable.mul_const

modified theorem interval_integral.interval_integrable_const

modified theorem interval_integral.interval_integrable_inv_one_add_sq

modified theorem interval_integral.interval_integrable_one_div_one_add_sq

modified theorem interval_integral.interval_integrable_pow